harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Init.lean
lemma forall_lt_succ : (∀ m < n + 1, p m) ↔ (∀ m < n, p m) ∧ p n

Proof state:
n : ℕ
p : ℕ → Prop
⊢ (∀ (m : ℕ), m < n + 1 → p m) ↔ (∀ (m : ℕ), m < n → p m) ∧ p n

Tactic:
simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq, or_comm, forall_eq_or_imp, and_comm]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem norm_equiv_symm_const' {β} [SeminormedAddCommGroup β] [Nonempty ι] (b : β) :
    ‖(WithLp.equiv p (ι → β)).symm (Function.const _ b)‖ =
      (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖b‖ :=
  (congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_equiv_symm_const' b).trans <| by simp

Proof state:
p : ℝ≥0∞
ι : Type u_2
hp : Fact (1 ≤ p)
inst✝² : Fintype ι
β : Type u_5
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
⊢ ↑(↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊) = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem isPathConnected_iff_pathConnectedSpace : IsPathConnected F ↔ PathConnectedSpace F

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ PathConnectedSpace ↑F

Tactic:
rw [pathConnectedSpace_iff_univ, IsInducing.subtypeVal.isPathConnected_iff, image_univ,
  Subtype.range_val_subtype, setOf_mem_eq]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem pow_succ' {n : ℕ} (h : n ≠ 0) : M ^ (n + 1) = M * M ^ n

Proof state:
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
⊢ M ^ (n + 1) = M * M ^ n

Tactic:
rw [add_comm, M.pow_add h, Submodule.pow_one]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_def {s : Unit →₀ ℕ} {n : ℕ} (h : s () = n) : coeff R n = MvPowerSeries.coeff R s

Proof state:
R : Type u_1
inst✝ : Semiring R
s : Unit →₀ ℕ
n : ℕ
h : s () = n
⊢ coeff R n = MvPowerSeries.coeff R s

Tactic:
rw [coeff, ← h, ← Finsupp.unique_single s]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Over.lean
lemma overEquiv_symm_mem_over {X : C} (Y : Over X) (S : Sieve Y.left) (hS : S ∈ J Y.left) :
    (Sieve.overEquiv Y).symm S ∈ (J.over X) Y

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y.left
hS : S ∈ J Y.left
⊢ (Sieve.overEquiv Y).symm S ∈ (J.over X) Y

Tactic:
simpa only [mem_over_iff, Equiv.apply_symm_apply] using hS

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem isUnit_fromBlocks_iff_of_invertible₁₁ {A : Matrix m m α} {B : Matrix m n α}
    {C : Matrix n m α} {D : Matrix n n α} [Invertible A] :
    IsUnit (fromBlocks A B C D) ↔ IsUnit (D - C * ⅟ A * B)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible A
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (D - C * ⅟A * B)

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
  (invertibleEquivFromBlocks₁₁Invertible A B C D).nonempty_congr]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
theorem trace_mul_cycle [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R)
    (C : Matrix p m R) : trace (A * B * C) = trace (C * A * B)

Proof state:
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (A * B * C).trace = (C * A * B).trace

Tactic:
rw [trace_mul_comm, Matrix.mul_assoc]

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem add_div_eq_mul_add_div (a b : K) (hc : c ≠ 0) : a + b / c = (a * c + b) / c :=
  (eq_div_iff_mul_eq hc).2 <| by rw [right_distrib, div_mul_cancel₀ _ hc]

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
c a b : K
hc : c ≠ 0
⊢ (a + b / c) * c = a * c + b

Tactic:
rw [right_distrib, div_mul_cancel₀ _ hc]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem left_ne_zero_of_oangle_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : x ≠ 0 :=
  o.left_ne_zero_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 1
⊢ 1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Opposites.lean
theorem opRingEquiv_symm_monomial (n : ℕ) (r : Rᵐᵒᵖ) :
    (opRingEquiv R).symm (monomial n r) = op (monomial n (unop r)) :=
  (opRingEquiv R).injective (by simp)

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : Rᵐᵒᵖ
⊢ (opRingEquiv R) ((opRingEquiv R).symm ((monomial n) r)) = (opRingEquiv R) (op ((monomial n) (unop r)))

Tactic:
simp

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

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

Tactic:
simp only [LeftTotal, IsEmpty.exists_iff, isEmpty_iff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_take_mul_prod_drop (L : List M) (i : ℕ) :
    (L.take i).prod * (L.drop i).prod = L.prod

Proof state:
M : Type u_4
inst✝ : Monoid M
L : List M
i : ℕ
⊢ (take i L).prod * (drop i L).prod = L.prod

Tactic:
simp [← prod_append]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsRestriction.antisymm {M' : Matroid α} (h : M ≤r M') (h' : M' ≤r M) : M = M'

Proof state:
α : Type u_1
M M' : Matroid α
h : M ≤r M'
h' : M' ≤r M
⊢ M = M'

Tactic:
simpa using (ofMatroid_le_iff.2 h).antisymm (ofMatroid_le_iff.2 h')

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma le_rpow_inv_iff_of_pos (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 < z) : x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Proof state:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
rw [← rpow_le_rpow_iff hx _ hz, rpow_inv_rpow] <;> positivity

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem nsmul : a ≡ b [PMOD p] → n • a ≡ n • b [PMOD n • p] :=
  Exists.imp fun m hm => by rw [← smul_sub, hm, smul_comm]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
n : ℕ
m : ℤ
hm : b - a = m • p
⊢ n • b - n • a = m • n • p

Tactic:
rw [← smul_sub, hm, smul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_eq_of_eq_mul_left {a b c : Int}
    (H1 : b ≠ 0) (H2 : a = c * b) : a.tdiv b = c :=
  Int.tdiv_eq_of_eq_mul_right H1 (by rw [Int.mul_comm, H2])

Proof state:
a b c : Int
H1 : b ≠ 0
H2 : a = c * b
⊢ a = b * c

Tactic:
rw [Int.mul_comm, H2]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Basic.lean
theorem comp_right_eq_zero [IsIso g] : f ≫ g = 0 ↔ f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso g
⊢ f ≫ g = 0 ↔ f = 0

Tactic:
rw [← IsIso.eq_comp_inv, Limits.zero_comp]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem antilipschitz_of_norm_ge {K : ℝ≥0} (h : ∀ x, ‖x‖ ≤ K * ‖f x‖) : AntilipschitzWith K f :=
  AntilipschitzWith.of_le_mul_dist fun x y => by simpa only [dist_eq_norm, map_sub] using h (x - y)

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : ℝ≥0
h : ∀ (x : V₁), ‖x‖ ≤ ↑K * ‖f x‖
x y : V₁
⊢ dist x y ≤ ↑K * dist (f x) (f y)

Tactic:
simpa only [dist_eq_norm, map_sub] using h (x - y)

Result:
no goals
-- Mathlib/RingTheory/PowerBasis.lean
theorem constr_pow_gen (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0) :
    pb.basis.constr A (fun i => y ^ (i : ℕ)) pb.gen = y

Proof state:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
⊢ ((pb.basis.constr A) fun i => y ^ ↑i) pb.gen = y

Tactic:
convert pb.constr_pow_aeval hy X <;> rw [aeval_X]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_one_left_iff (n : ℕ) : Coprime 1 n ↔ True

Proof state:
n : ℕ
⊢ Coprime 1 n ↔ True

Tactic:
simp [Coprime]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma ceilRoot_eq_zero : ceilRoot n a = 0 ↔ n = 0 ∨ a = 0 :=
  ceilRoot_ne_zero.not_right.trans <| by simp only [not_and_or, ne_eq, not_not]

Proof state:
a n : ℕ
⊢ ¬(n ≠ 0 ∧ a ≠ 0) ↔ n = 0 ∨ a = 0

Tactic:
simp only [not_and_or, ne_eq, not_not]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/OfSection.lean
lemma mem_ofSection_obj : x ∈ (ofSection x).obj X := ⟨𝟙 _, by simp⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
⊢ F.map (𝟙 X) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Chain.lean
lemma isChain_union {s t : Set α} :
    IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a

Proof state:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a

Tactic:
rw [IsChain, IsChain, IsChain, pairwise_union_of_symmetric fun _ _ ↦ Or.symm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem Complex.volume_closedBall (a : ℂ) (r : ℝ) :
    volume (Metric.closedBall a r) = .ofReal r ^ 2 * NNReal.pi

Proof state:
a : ℂ
r : ℝ
⊢ volume (Metric.closedBall a r) = ENNReal.ofReal r ^ 2 * ↑NNReal.pi

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, Complex.volume_ball]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem convexHull_add (s t : Set E) : convexHull R (s + t) = convexHull R s + convexHull R t

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s t : Set E
⊢ (convexHull R) (s + t) = (convexHull R) s + (convexHull R) t

Tactic:
simp_rw [← add_image_prod, ← IsLinearMap.isLinearMap_add.image_convexHull, convexHull_prod]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive (attr := simp)]
protected lemma mul_div_cancel_right (h : IsUnit b) (a : α) : a * b / b = a

Proof state:
α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a * b / b = a

Tactic:
rw [div_eq_mul_inv, h.mul_inv_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem apply_mulIndicator_symmDiff {g : G → β} (hg : ∀ x, g x⁻¹ = g x)
    (s t : Set α) (f : α → G) (x : α) :
    g (mulIndicator (s ∆ t) f x) = g (mulIndicator s f x / mulIndicator t f x)

Proof state:
α : Type u_1
β : Type u_2
G : Type u_5
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
by_cases hs : x ∈ s <;> by_cases ht : x ∈ t <;> simp [mem_symmDiff, *]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
/-- This lemma justifies its existence from its utility in crystallographic root system theory. -/
lemma mul_mem_zero_one_two_three_four_iff {a b : ℤ} (h₀ : a = 0 ↔ b = 0) :
    a * b ∈ ({0, 1, 2, 3, 4} : Set ℤ) ↔ (a, b) ∈ ({
      (0, 0),
      (1, 1), (-1, -1),
      (1, 2), (2, 1), (-1, -2), (-2, -1),
      (1, 3), (3, 1), (-1, -3), (-3, -1),
      (4, 1), (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)} : Set (ℤ × ℤ))

Proof state:
a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ a * b = 0 ∨
      (a, b) ∈ divisorsAntidiag 1 ∨
        (a, b) ∈ divisorsAntidiag 2 ∨ (a, b) ∈ divisorsAntidiag 3 ∨ (a, b) ∈ divisorsAntidiag 4 ↔
    (a, b) = (0, 0) ∨
      (a, b) = (1, 1) ∨
        (a, b) = (-1, -1) ∨
          (a, b) = (1, 2) ∨
            (a, b) = (2, 1) ∨
              (a, b) = (-1, -2) ∨
                (a, b) = (-2, -1) ∨
                  (a, b) = (1, 3) ∨
                    (a, b) = (3, 1) ∨
                      (a, b) = (-1, -3) ∨
                        (a, b) = (-3, -1) ∨
                          (a, b) = (4, 1) ∨
                            (a, b) = (1, 4) ∨
                              (a, b) = (-4, -1) ∨ (a, b) = (-1, -4) ∨ (a, b) = (2, 2) ∨ (a, b) = (-2, -2)

Tactic:
aesop

Result:
no goals

Proof state:
a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ a * b ∈ {0, 1, 2, 3, 4} ↔
    (a, b) ∈
      {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
        (-4, -1), (-1, -4), (2, 2), (-2, -2)}

Tactic:
simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
  one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]

Result:
a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ a * b = 0 ∨
      (a, b) ∈ divisorsAntidiag 1 ∨
        (a, b) ∈ divisorsAntidiag 2 ∨ (a, b) ∈ divisorsAntidiag 3 ∨ (a, b) ∈ divisorsAntidiag 4 ↔
    (a, b) = (0, 0) ∨
      (a, b) = (1, 1) ∨
        (a, b) = (-1, -1) ∨
          (a, b) = (1, 2) ∨
            (a, b) = (2, 1) ∨
              (a, b) = (-1, -2) ∨
                (a, b) = (-2, -1) ∨
                  (a, b) = (1, 3) ∨
                    (a, b) = (3, 1) ∨
                      (a, b) = (-1, -3) ∨
                        (a, b) = (-3, -1) ∨
                          (a, b) = (4, 1) ∨
                            (a, b) = (1, 4) ∨
                              (a, b) = (-4, -1) ∨ (a, b) = (-1, -4) ∨ (a, b) = (2, 2) ∨ (a, b) = (-2, -2)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem signExtend_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h1 : x = x') :
    BitVec.signExtend n x' = BitVec.signExtend n x

Proof state:
n w : Nat
x x' : BitVec w
h1 : x = x'
⊢ BitVec.signExtend n x' = BitVec.signExtend n x

Tactic:
simp[*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem tail_iota (n : Nat) : (iota n).tail = iota (n - 1)

Proof state:
n : Nat
⊢ (iota n).tail = iota (n - 1)

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_to_int {α} [AddGroupWithOne α] (n : Num) : ((n : ℤ) : α) = n

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : Num
⊢ ↑↑n = ↑n

Tactic:
rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem exists_countable_dense_bot_top (α : Type*) [TopologicalSpace α] [SeparableSpace α]
    [PartialOrder α] :
    ∃ s : Set α, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∈ s) ∧ ∀ x, IsTop x → x ∈ s

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : PartialOrder α
⊢ ∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop x → x ∈ s

Tactic:
simpa using dense_univ.exists_countable_dense_subset_bot_top

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_lt_mul_inv_iff' : a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c d : α
⊢ a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b

Tactic:
rw [mul_comm c, mul_inv_lt_inv_mul_iff, mul_comm]

Result:
no goals
-- Mathlib/Topology/DiscreteSubset.lean
lemma mem_codiscrete_accPt {S : Set X} :
    S ∈ codiscrete X ↔ ∀ x, ¬AccPt x (𝓟 Sᶜ)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ S ∈ codiscrete X ↔ ∀ (x : X), ¬AccPt x (𝓟 Sᶜ)

Tactic:
simp only [mem_codiscrete, disjoint_iff, AccPt, not_neBot]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
@[to_additive]
lemma compl_mul_closure_one_eq_iff {t : Set G} :
    tᶜ * (closure {1} : Set G) = tᶜ ↔ t * (closure {1} : Set G) = t :=
  ⟨fun h ↦ by simpa using compl_mul_closure_one_eq h, fun h ↦ compl_mul_closure_one_eq h⟩

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
h : tᶜ * closure {1} = tᶜ
⊢ t * closure {1} = t

Tactic:
simpa using compl_mul_closure_one_eq h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma _root_.Real.enorm_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    ‖x ^ y‖ₑ = ‖x‖ₑ ^ y

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ ‖x ^ y‖ₑ = ‖x‖ₑ ^ y

Tactic:
simp [enorm, nnnorm_rpow_of_nonneg hx, coe_rpow_of_nonneg _ hy]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_nonneg_of_nonpos_of_nonpos [ExistsAddOfLE α] [MulPosMono α]
    [AddRightMono α] [AddRightReflectLE α]
    (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
ha : a ≤ 0
hb : b ≤ 0
⊢ 0 ≤ a * b

Tactic:
simpa only [zero_mul] using mul_le_mul_of_nonpos_right ha hb

Result:
no goals
-- Mathlib/Order/SuccPred/CompleteLinearOrder.lean
lemma csSup_mem_of_not_isSuccPrelimit
    (hne : s.Nonempty) (hbdd : BddAbove s) (hlim : ¬ IsSuccPrelimit (sSup s)) : sSup s ∈ s

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
obtain ⟨y, hy⟩ := not_forall_not.mp hlim

Result:
case intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
⊢ sSup s ∈ s

Proof state:
case intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
⊢ sSup s ∈ s

Tactic:
obtain ⟨i, his, hi⟩ := exists_lt_of_lt_csSup hne hy.lt

Result:
case intro.intro.intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
i : α
his : i ∈ s
hi : y < i
⊢ sSup s ∈ s

Proof state:
case intro.intro.intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
i : α
his : i ∈ s
hi : y < i
⊢ sSup s ∈ s

Tactic:
exact eq_of_le_of_not_lt (le_csSup hbdd his) (hy.2 hi) ▸ his

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem support_zero : support (0 : FreeAbelianGroup X) = ∅

Proof state:
X : Type u_1
⊢ support 0 = ∅

Tactic:
simp only [support, Finsupp.support_zero, AddMonoidHom.map_zero]

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem upperBounds_l_image (s : Set α) :
    upperBounds (l '' s) = u ⁻¹' upperBounds s :=
  Set.ext fun b => by simp [upperBounds, gc _ _]

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
b : β
⊢ b ∈ upperBounds (l '' s) ↔ b ∈ u ⁻¹' upperBounds s

Tactic:
simp [upperBounds, gc _ _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mod_mul_mod {a b c : Nat} : (a % c * b) % c = a * b % c

Proof state:
a b c : Nat
⊢ a % c * b % c = a * b % c

Tactic:
rw [mul_mod, mod_mod, ← mul_mod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) :
    (Const.alter m k f).size ≤ m.size + 1

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).size ≤ m.size + 1

Tactic:
simp_to_raw using Raw₀.Const.size_alter_le_size

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem hom_zero_zero (f : ⦋0⦌ ⟶ ⦋0⦌) : f = 𝟙 _

Proof state:
f : ⦋0⦌ ⟶ ⦋0⦌
⊢ f = 𝟙 ⦋0⦌

Tactic:
apply Subsingleton.elim

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem bind₂_monomial (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ) (r : R) :
    bind₂ f (monomial d r) = f r * monomial d 1

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
r : R
⊢ (bind₂ f) ((monomial d) r) = f r * (monomial d) 1

Tactic:
simp only [monomial_eq, RingHom.map_mul, bind₂_C_right, Finsupp.prod, map_prod,
  map_pow, bind₂_X_right, C_1, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_ne_nil_iff (s : Nat) {n step : Nat} : range' s n step ≠ [] ↔ n ≠ 0

Proof state:
s n step : Nat
⊢ range' s n step ≠ [] ↔ n ≠ 0

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
theorem lift_comp_preservesLimitIso_hom (t : Cone F) :
    G.map (limit.lift _ t) ≫ (preservesLimitIso G F).hom =
    limit.lift (F ⋙ G) (G.mapCone _)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝² : Category.{w', w} J
F : J ⥤ C
inst✝¹ : PreservesLimit F G
inst✝ : HasLimit F
t : Cone F
⊢ G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom = limit.lift (F ⋙ G) (G.mapCone t)

Tactic:
ext

Result:
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝² : Category.{w', w} J
F : J ⥤ C
inst✝¹ : PreservesLimit F G
inst✝ : HasLimit F
t : Cone F
j✝ : J
⊢ (G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom) ≫ limit.π (F ⋙ G) j✝ =
    limit.lift (F ⋙ G) (G.mapCone t) ≫ limit.π (F ⋙ G) j✝

Proof state:
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝² : Category.{w', w} J
F : J ⥤ C
inst✝¹ : PreservesLimit F G
inst✝ : HasLimit F
t : Cone F
j✝ : J
⊢ (G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom) ≫ limit.π (F ⋙ G) j✝ =
    limit.lift (F ⋙ G) (G.mapCone t) ≫ limit.π (F ⋙ G) j✝

Tactic:
simp [← G.map_comp]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_restrictFreeVar' [DecidableEq α] {n : ℕ} {φ : L.BoundedFormula α n} {s : Set α}
    (h : ↑φ.freeVarFinset ⊆ s) {v : α → M} {xs : Fin n → M} :
    (φ.restrictFreeVar (Set.inclusion h)).Realize (v ∘ (↑)) xs ↔ φ.Realize v xs :=
  realize_restrictFreeVar _ (by simp)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
s : Set α
h : ↑φ.freeVarFinset ⊆ s
v : α → M
xs : Fin n → M
⊢ ∀ (a : { x // x ∈ φ.freeVarFinset }), (v ∘ Subtype.val) (Set.inclusion h a) = v ↑a

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem ex_iff_not_all_not (φ : L.BoundedFormula α (n + 1)) :
    φ.ex ⇔[T] φ.not.all.not := fun M v xs => by simp

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α (n + 1)
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (∃'φ ⇔ ∼(∀'∼φ)).Realize v xs

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Idempotent.lean
lemma map {M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {e : M}
    (he : IsIdempotentElem e) (f : F) : IsIdempotentElem (f e)

Proof state:
M : Type u_4
N : Type u_5
F : Type u_6
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M
he : IsIdempotentElem e
f : F
⊢ IsIdempotentElem (f e)

Tactic:
rw [IsIdempotentElem, ← map_mul, he.eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Basic.lean
theorem ofBool_true  : ofBool true  = 1

Proof state:
⊢ ofBool true = 1

Tactic:
trivial

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
lemma lt_slope_of_hasDerivWithinAt_Iio (hfc : StrictConcaveOn ℝ S f)
    (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Iio y) y) :
    f' < slope f x y

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ f' < slope f x y

Tactic:
simpa only [Pi.neg_def, slope_neg, neg_neg] using
  neg_lt_neg (hfc.neg.slope_lt_of_hasDerivWithinAt_Iio hx hy hxy hf'.neg)

Result:
no goals