harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem inner_rotation_pi_div_two_left_smul (x : V) (r : ℝ) :
    ⟪o.rotation (π / 2 : ℝ) x, r • x⟫ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ inner ((o.rotation ↑(π / 2)) x) (r • x) = 0

Tactic:
rw [inner_smul_right, inner_rotation_pi_div_two_left, mul_zero]

Result:
no goals
-- Mathlib/Data/Matrix/Bilinear.lean
theorem mulRightLinearMap_mul [IsScalarTower R A A] (a : Matrix m n A) (b : Matrix n o A) :
    mulRightLinearMap l R (a * b) = (mulRightLinearMap l R b).comp (mulRightLinearMap l R a)

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m n A
b : Matrix n o A
⊢ mulRightLinearMap l R (a * b) = mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a

Tactic:
ext

Result:
case h.a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m n A
b : Matrix n o A
x✝ : Matrix l m A
i✝ : l
j✝ : o
⊢ (mulRightLinearMap l R (a * b)) x✝ i✝ j✝ = (mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a) x✝ i✝ j✝

Proof state:
case h.a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m n A
b : Matrix n o A
x✝ : Matrix l m A
i✝ : l
j✝ : o
⊢ (mulRightLinearMap l R (a * b)) x✝ i✝ j✝ = (mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a) x✝ i✝ j✝

Tactic:
simp only [mulRightLinearMap_apply, LinearMap.comp_apply, Matrix.mul_assoc]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
@[simp]
lemma zmod_val_inv_nsmul_nsmul (hn : (Nat.card α).Coprime n) (a : α) :
    (n⁻¹ : ZMod (Nat.card α)).val • n • a = a

Proof state:
α : Type u_1
inst✝ : AddGroup α
n : ℕ
hn : (Nat.card α).Coprime n
a : α
⊢ (↑n)⁻¹.val • n • a = a

Tactic:
rw [nsmul_left_comm, nsmul_zmod_val_inv_nsmul hn]

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem pi_liftQ_eq_liftQ_pi {ι : Type*} {N : ι → Type*}
    [∀ i, AddCommGroup (N i)] [∀ i, Module R (N i)]
    (f : (i : ι) → M →ₗ[R] (N i)) {p : Submodule R M} (h : ∀ i, p ≤ ker (f i)) :
    LinearMap.pi (fun i ↦ p.liftQ (f i) (h i)) =
      p.liftQ (LinearMap.pi f) (LinearMap.ker_pi f ▸ le_iInf h)

Proof state:
case h.h.h
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_5
N : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M →ₗ[R] N i
p : Submodule R M
h : ∀ (i : ι), p ≤ ker (f i)
x : M
i : ι
⊢ ((LinearMap.pi fun i => p.liftQ (f i) ⋯) ∘ₗ p.mkQ) x i = (p.liftQ (LinearMap.pi f) ⋯ ∘ₗ p.mkQ) x i

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_5
N : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M →ₗ[R] N i
p : Submodule R M
h : ∀ (i : ι), p ≤ ker (f i)
⊢ (LinearMap.pi fun i => p.liftQ (f i) ⋯) = p.liftQ (LinearMap.pi f) ⋯

Tactic:
ext x i

Result:
case h.h.h
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_5
N : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M →ₗ[R] N i
p : Submodule R M
h : ∀ (i : ι), p ≤ ker (f i)
x : M
i : ι
⊢ ((LinearMap.pi fun i => p.liftQ (f i) ⋯) ∘ₗ p.mkQ) x i = (p.liftQ (LinearMap.pi f) ⋯ ∘ₗ p.mkQ) x i
-- Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@[to_additive (attr := simp)]
lemma _root_.Cardinal.mk_inv (s : Set G) : #↥(s⁻¹) = #s

Proof state:
G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ #↑s⁻¹ = #↑s

Tactic:
rw [← image_inv_eq_inv, Cardinal.mk_image_eq_of_injOn _ _ inv_injective.injOn]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_snoc [CommMonoid β] {n : ℕ} (x : β) (f : Fin n → β) :
    (∏ i : Fin n.succ, (snoc f x : Fin n.succ → β) i) = (∏ i : Fin n, f i) * x

Proof state:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
x : β
f : Fin n → β
⊢ ∏ i : Fin n.succ, snoc f x i = (∏ i : Fin n, f i) * x

Tactic:
simp [prod_univ_castSucc]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem bodd_bit (b n) : bodd (bit b n) = b

Proof state:
n : ℤ
⊢ bodd 2 = false

Tactic:
rfl

Result:
no goals

Proof state:
b : Bool
n : ℤ
⊢ (2 * n + bif b then 1 else 0).bodd = b

Tactic:
cases b <;> cases bodd n <;> simp [(show bodd 2 = false by rfl)]

Result:
no goals

Proof state:
b : Bool
n : ℤ
⊢ (bit b n).bodd = b

Tactic:
rw [bit_val]

Result:
b : Bool
n : ℤ
⊢ (2 * n + bif b then 1 else 0).bodd = b
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Step.append_right : ∀ {L₁ L₂ L₃ : List (α × Bool)}, Step L₁ L₂ → Step (L₁ ++ L₃) (L₂ ++ L₃)
  | _, _, _, Red.Step.not => by simp

Proof state:
α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝ ++ x✝¹) (L₁✝ ++ L₂✝ ++ x✝¹)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_lt (ha : 0 < a) (hb : 0 < b) : 1 / a < b ↔ 1 / b < a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 < a
hb : 0 < b
⊢ 1 / a < b ↔ 1 / b < a

Tactic:
simpa using inv_lt_comm₀ ha hb

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Under/Basic.lean
@[reassoc (attr := simp)]
lemma pushout_inr_tensorProdObjIsoPushoutObj_inv_right (A : Under R) :
    pushout.inr A.hom (ofHom <| algebraMap R S) ≫
      (tensorProdObjIsoPushoutObj S A).inv.right =
      (CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom)

Proof state:
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A : Under R
⊢ pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫ (tensorProdObjIsoPushoutObj S A).inv.right =
    ofHom Algebra.TensorProduct.includeLeftRingHom

Tactic:
simp [tensorProdObjIsoPushoutObj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem zero_shiftLeft : ∀ n, 0 <<< n = 0
  | 0 => by simp [shiftLeft]
  | n + 1 => by simp [shiftLeft, zero_shiftLeft n, shiftLeft_succ]

Proof state:
n : Nat
⊢ 0 <<< (n + 1) = 0

Tactic:
simp [shiftLeft, zero_shiftLeft n, shiftLeft_succ]

Result:
no goals

Proof state:
⊢ 0 <<< 0 = 0

Tactic:
simp [shiftLeft]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem smul_leftMulMatrix {G} [Group G] [DistribMulAction G S]
    [SMulCommClass G R S] [SMulCommClass G S S] (g : G) (x) :
    leftMulMatrix (g • b) x = leftMulMatrix b x

Proof state:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
m : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
b : Basis m R S
G : Type u_4
inst✝³ : Group G
inst✝² : DistribMulAction G S
inst✝¹ : SMulCommClass G R S
inst✝ : SMulCommClass G S S
g : G
x : S
⊢ (leftMulMatrix (g • b)) x = (leftMulMatrix b) x

Tactic:
ext

Result:
case a
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
m : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
b : Basis m R S
G : Type u_4
inst✝³ : Group G
inst✝² : DistribMulAction G S
inst✝¹ : SMulCommClass G R S
inst✝ : SMulCommClass G S S
g : G
x : S
i✝ j✝ : m
⊢ (leftMulMatrix (g • b)) x i✝ j✝ = (leftMulMatrix b) x i✝ j✝

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
m : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
b : Basis m R S
G : Type u_4
inst✝³ : Group G
inst✝² : DistribMulAction G S
inst✝¹ : SMulCommClass G R S
inst✝ : SMulCommClass G S S
g : G
x : S
i✝ j✝ : m
⊢ (leftMulMatrix (g • b)) x i✝ j✝ = (leftMulMatrix b) x i✝ j✝

Tactic:
simp_rw [leftMulMatrix_apply, LinearMap.toMatrix_apply, coe_lmul_eq_mul, LinearMap.mul_apply',
  Basis.repr_smul, Basis.smul_apply, LinearEquiv.trans_apply,
  DistribMulAction.toLinearEquiv_symm_apply, mul_smul_comm, inv_smul_smul]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
@[simp] lemma sdiff_singleton (s : UpperSet α) (a : α) : s.sdiff {a} = s.erase a

Proof state:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s.erase a

Tactic:
simp [sdiff, erase]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem tendsto_one_iff_norm_tendsto_zero {f : α → E} {a : Filter α} :
    Tendsto f a (𝓝 1) ↔ Tendsto (‖f ·‖) a (𝓝 0) :=
  tendsto_iff_norm_div_tendsto_zero.trans <| by simp only [div_one]

Proof state:
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
f : α → E
a : Filter α
⊢ Tendsto (fun e => ‖f e / 1‖) a (𝓝 0) ↔ Tendsto (fun x => ‖f x‖) a (𝓝 0)

Tactic:
simp only [div_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/LineDeriv.lean
theorem IsExtrFilter.hasLineDerivAt_eq_zero {l : Filter E} (h : IsExtrFilter f l a)
    (hd : HasLineDerivAt ℝ f f' a b) (h' : Tendsto (fun t : ℝ ↦ a + t • b) (𝓝 0) l) : f' = 0 :=
  IsLocalExtr.hasDerivAt_eq_zero (IsExtrFilter.comp_tendsto (by simpa using h) h') hd

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E → ℝ
a b : E
f' : ℝ
l : Filter E
h : IsExtrFilter f l a
hd : HasLineDerivAt ℝ f f' a b
h' : Tendsto (fun t => a + t • b) (𝓝 0) l
⊢ IsExtrFilter f l (a + 0 • b)

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
@[to_additive]
lemma id_apply (X : Grp) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : Grp
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_norm_right : (f =O[l] fun x => ‖g' x‖) ↔ f =O[l] g'

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∃ c, IsBigOWith c l f fun x => ‖g' x‖) ↔ ∃ c, IsBigOWith c l f g'

Tactic:
exact exists_congr fun _ => isBigOWith_norm_right

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =O[l] fun x => ‖g' x‖) ↔ f =O[l] g'

Tactic:
simp only [IsBigO_def]

Result:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∃ c, IsBigOWith c l f fun x => ‖g' x‖) ↔ ∃ c, IsBigOWith c l f g'
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ico_succ_succ_eq_Ioc (a b : α) : Ico (succ a) (succ b) = Ioc a b := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ ↑(Ico (succ a) (succ b)) = ↑(Ioc a b)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
    arr.foldrM f init = arr.toList.reverse.foldlM (fun x y => f y x) init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr✝ : Array α
this : arr✝ = #[] ∨ 0 < arr✝.size
arr : Array α
h : 0 < arr.size
⊢ foldrM f init arr = List.foldlM (fun x y => f y x) init arr.toList.reverse

Tactic:
simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
⊢ foldrM f init arr = List.foldlM (fun x y => f y x) init arr.toList.reverse

Tactic:
have : arr = #[] ∨ 0 < arr.size :=
  match arr with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
this : arr = #[] ∨ 0 < arr.size
⊢ foldrM f init arr = List.foldlM (fun x y => f y x) init arr.toList.reverse

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
this : arr = #[] ∨ 0 < arr.size
⊢ foldrM f init arr = List.foldlM (fun x y => f y x) init arr.toList.reverse

Tactic:
match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr✝ : Array α
this : arr✝ = #[] ∨ 0 < arr✝.size
arr : Array α
h : 0 < arr.size
⊢ foldrM f init arr = List.foldlM (fun x y => f y x) init arr.toList.reverse

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
this : arr = #[] ∨ 0 < arr.size
⊢ foldrM f init #[] = List.foldlM (fun x y => f y x) init #[].toList.reverse

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive nnnorm_nsmul_le]
lemma nnnorm_pow_le_mul_norm {n : ℕ} : ‖a ^ n‖₊ ≤ n * ‖a‖₊

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℕ
⊢ ‖a ^ n‖₊ ≤ ↑n * ‖a‖₊

Tactic:
simpa only [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_natCast] using norm_pow_le_mul_norm

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_two_mul : sin (2 * x) = 2 * sin x * cos x :=
  ofReal_injective <| by simp [sin_two_mul]

Proof state:
x : ℝ
⊢ ↑(sin (2 * x)) = ↑(2 * sin x * cos x)

Tactic:
simp [sin_two_mul]

Result:
no goals
-- Mathlib/Algebra/FreeMonoid/Basic.lean
theorem map_apply_map_symm_eq {x : FreeMonoid β} (e : α ≃ β) :
    (map ⇑e) ((map ⇑e.symm) x) = x

Proof state:
α : Type u_1
β : Type u_2
x : FreeMonoid β
e : α ≃ β
⊢ (map ⇑e) ((map ⇑e.symm) x) = x

Tactic:
simp [map_map]

Result:
no goals
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem exp_add' (dp : ℕ → A → A)
    (dp_add : ∀ n, dp n (a + b) = (antidiagonal n).sum fun k ↦ dp k.1 a * dp k.2 b) :
    PowerSeries.mk (fun n ↦ dp n (a + b)) =
      (PowerSeries.mk fun n ↦ dp n a) * (PowerSeries.mk fun n ↦ dp n b)

Proof state:
A : Type u_1
inst✝ : CommSemiring A
a b : A
dp : ℕ → A → A
dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ antidiagonal n, dp k.1 a * dp k.2 b
⊢ (PowerSeries.mk fun n => dp n (a + b)) = (PowerSeries.mk fun n => dp n a) * PowerSeries.mk fun n => dp n b

Tactic:
ext n

Result:
case h
A : Type u_1
inst✝ : CommSemiring A
a b : A
dp : ℕ → A → A
dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ antidiagonal n, dp k.1 a * dp k.2 b
n : ℕ
⊢ (PowerSeries.coeff A n) (PowerSeries.mk fun n => dp n (a + b)) =
    (PowerSeries.coeff A n) ((PowerSeries.mk fun n => dp n a) * PowerSeries.mk fun n => dp n b)

Proof state:
case h
A : Type u_1
inst✝ : CommSemiring A
a b : A
dp : ℕ → A → A
dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ antidiagonal n, dp k.1 a * dp k.2 b
n : ℕ
⊢ (PowerSeries.coeff A n) (PowerSeries.mk fun n => dp n (a + b)) =
    (PowerSeries.coeff A n) ((PowerSeries.mk fun n => dp n a) * PowerSeries.mk fun n => dp n b)

Tactic:
simp only [exp, PowerSeries.coeff_mk, PowerSeries.coeff_mul, dp_add n,
  sum_antidiagonal_eq_sum_range_succ_mk]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
    (f₃ : X₃ ⟶ Y₃) :
    coprod.map (coprod.map f₁ f₂) f₃ ≫ (coprod.associator Y₁ Y₂ Y₃).hom =
      (coprod.associator X₁ X₂ X₃).hom ≫ coprod.map f₁ (coprod.map f₂ f₃)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ map (map f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom = (associator X₁ X₂ X₃).hom ≫ map f₁ (map f₂ f₃)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem self_lt_rpow_of_lt_one (h₁ : 0 < x) (h₂ : x < 1) (h₃ : y < 1) : x < x ^ y

Proof state:
x y : ℝ
h₁ : 0 < x
h₂ : x < 1
h₃ : y < 1
⊢ x < x ^ y

Tactic:
simpa only [rpow_one] using rpow_lt_rpow_of_exponent_gt h₁ h₂ h₃

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem orderTop_add_le_mul {x y : HahnSeries Γ R} :
    x.orderTop + y.orderTop ≤ (x * y).orderTop

Proof state:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ x.orderTop + y.orderTop ≤ (x * y).orderTop

Tactic:
rw [← smul_eq_mul]

Result:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ x.orderTop + y.orderTop ≤ (x • y).orderTop

Proof state:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ x.orderTop + y.orderTop ≤ (x • y).orderTop

Tactic:
exact HahnModule.orderTop_vAdd_le_orderTop_smul fun i j ↦ rfl

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem mod_coprime {a b : ℕ} (hab : Nat.Coprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b] :=
  ⟨Nat.gcdA a b,
    have hgcd : Nat.gcd a b = 1 := Nat.Coprime.gcd_eq_one hab
    calc
      ↑a * Nat.gcdA a b ≡ ↑a * Nat.gcdA a b + ↑b * Nat.gcdB a b [ZMOD ↑b] :=
        ModEq.symm <| modEq_add_fac _ <| ModEq.refl _
      _ ≡ 1 [ZMOD ↑b]

Proof state:
a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑a * a.gcdA b + ↑b * a.gcdB b ≡ 1 [ZMOD ↑b]

Tactic:
rw [← Nat.gcd_eq_gcd_ab, hgcd]

Result:
a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑1 ≡ 1 [ZMOD ↑b]

Proof state:
a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑1 ≡ 1 [ZMOD ↑b]

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_lt_log_iff (hx : 0 < x) (hy : 0 < y) : log x < log y ↔ x < y

Proof state:
x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y

Tactic:
rw [← exp_lt_exp, exp_log hx, exp_log hy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem replicate_succ {x : BitVec w} :
    x.replicate (n + 1) =
    (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega)

Proof state:
w n : Nat
x : BitVec w
⊢ w + w * n = w * (n + 1)

Tactic:
rw [Nat.mul_succ]

Result:
w n : Nat
x : BitVec w
⊢ w + w * n = w * n + w

Proof state:
w n : Nat
x : BitVec w
⊢ w + w * n = w * n + w

Tactic:
omega

Result:
no goals

Proof state:
w n : Nat
x : BitVec w
⊢ replicate (n + 1) x = BitVec.cast ⋯ (x ++ replicate n x)

Tactic:
simp [replicate]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_not_succ_of_ne_sup {ι : Type u} {f : ι → Ordinal.{max u v}}
    (hf : ∀ i, f i ≠ sup.{_, v} f) {a} (hao : a < sup.{_, v} f) : succ a < sup.{_, v} f

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ (i : ι), f i ≠ sup f
a : Ordinal.{max u v}
hao : a < sup f
hoa : sup f ≤ succ a
⊢ False

Tactic:
exact
  hao.not_le (sup_le fun i => le_of_lt_succ <| (lt_of_le_of_ne (le_sup _ _) (hf i)).trans_le hoa)

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ (i : ι), f i ≠ sup f
a : Ordinal.{max u v}
hao : a < sup f
⊢ succ a < sup f

Tactic:
by_contra! hoa

Result:
ι : Type u
f : ι → Ordinal.{max u v}
hf : ∀ (i : ι), f i ≠ sup f
a : Ordinal.{max u v}
hao : a < sup f
hoa : sup f ≤ succ a
⊢ False
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_le (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (x : R) :
    seminormFromBounded' f x ≤ c * f x

Proof state:
case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : 0 y < f y
⊢ f (x * y) / f y ≤ c * f x

Tactic:
rw [div_le_iff₀ hy]

Result:
case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : 0 y < f y
⊢ f (x * y) ≤ c * f x * f y

Proof state:
case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : f y = 0 y
⊢ f (x * y) / f y ≤ c * f x

Tactic:
simpa [hy] using seminormFromBounded_aux f_nonneg f_mul x

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : 0 y < f y
⊢ f (x * y) ≤ c * f x * f y

Tactic:
apply f_mul

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ seminormFromBounded' f x ≤ c * f x

Tactic:
refine ciSup_le (fun y ↦ ?_)

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
⊢ f (x * y) / f y ≤ c * f x

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
⊢ f (x * y) / f y ≤ c * f x

Tactic:
rcases (f_nonneg y).eq_or_gt with hy | hy

Result:
case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : f y = 0 y
⊢ f (x * y) / f y ≤ c * f x

case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : 0 y < f y
⊢ f (x * y) / f y ≤ c * f x
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem map_hausdorffMeasure (e : X ≃ᵢ Y) (d : ℝ) : Measure.map e μH[d] = μH[d]

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
e : X ≃ᵢ Y
d : ℝ
⊢ Measure.map ⇑e μH[d] = μH[d]

Tactic:
rw [e.isometry.map_hausdorffMeasure (Or.inr e.surjective), e.surjective.range_eq, restrict_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_cons_of_isSome (l) (h : (f a).isSome) : findSome? f (a :: l) = f a

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
h : (f a).isSome = true
⊢ findSome? f (a :: l) = f a

Tactic:
simp only [findSome?]

Result:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
h : (f a).isSome = true
⊢ (match f a with
    | some b => some b
    | none => findSome? f l) =
    f a

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
h : (f a).isSome = true
⊢ (match f a with
    | some b => some b
    | none => findSome? f l) =
    f a

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem head?_mapIdx {l : List α} {f : Nat → α → β} : (mapIdx f l).head? = l.head?.map (f 0)

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
⊢ (mapIdx f l).head? = Option.map (f 0) l.head?

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_div_inv : a⁻¹ / b⁻¹ = b / a

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ a⁻¹ / b⁻¹ = b / a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem exists_of_mem_mapIdx {b : β} {l : Vector α n}
    (h : b ∈ l.mapIdx f) : ∃ (i : Nat) (h : i < n), f i l[i] = b

Proof state:
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
b : β
l : Vector α n
h : b ∈ l.mapFinIdx fun i a x => f i a
⊢ ∃ i h, f i l[i] = b

Tactic:
simpa [Fin.exists_iff] using exists_of_mem_mapFinIdx h

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
b : β
l : Vector α n
h : b ∈ mapIdx f l
⊢ ∃ i h, f i l[i] = b

Tactic:
rw [mapIdx_eq_mapFinIdx] at h

Result:
β : Type u_1
α : Type u_2
n : Nat
f : Nat → α → β
b : β
l : Vector α n
h : b ∈ l.mapFinIdx fun i a x => f i a
⊢ ∃ i h, f i l[i] = b
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Ioi : (some : α → WithTop α) '' Ioi a = Ioo (a : WithTop α) ⊤

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Ioi a = Ioo ↑a ⊤

Tactic:
rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem toReal_setLaverage {f : α → ℝ≥0∞} (hf : AEMeasurable f (μ.restrict s))
    (hf' : ∀ᵐ x ∂μ.restrict s, f x ≠ ∞) :
    (⨍⁻ x in s, f x ∂μ).toReal = ⨍ x in s, (f x).toReal ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.restrict s)
hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ⊤
⊢ (⨍⁻ (x : α) in s, f x ∂μ).toReal = ⨍ (x : α) in s, (f x).toReal ∂μ

Tactic:
simpa [laverage_eq] using toReal_laverage hf hf'

Result:
no goals