harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_zero' : taylor (0 : R) = LinearMap.id

Proof state:
case h.h.a
R : Type u_1
inst✝ : Semiring R
n✝¹ n✝ : ℕ
⊢ ((taylor 0 ∘ₗ monomial n✝¹) 1).coeff n✝ = ((LinearMap.id ∘ₗ monomial n✝¹) 1).coeff n✝

Tactic:
simp only [taylor_apply, add_zero, comp_X, _root_.map_zero, LinearMap.id_comp,
  Function.comp_apply, LinearMap.coe_comp]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ taylor 0 = LinearMap.id

Tactic:
ext

Result:
case h.h.a
R : Type u_1
inst✝ : Semiring R
n✝¹ n✝ : ℕ
⊢ ((taylor 0 ∘ₗ monomial n✝¹) 1).coeff n✝ = ((LinearMap.id ∘ₗ monomial n✝¹) 1).coeff n✝
-- Mathlib/Algebra/Module/ZMod.lean
theorem map_smul (f : F) (c : ZMod n) (x : M) : f (c • x) = c • f x

Proof state:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₁
inst✝³ : FunLike F M M₁
inst✝² : AddMonoidHomClass F M M₁
inst✝¹ : Module (ZMod n) M
inst✝ : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ f (c • x) = c • f x

Tactic:
rw [← ZMod.intCast_zmod_cast c]

Result:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₁
inst✝³ : FunLike F M M₁
inst✝² : AddMonoidHomClass F M M₁
inst✝¹ : Module (ZMod n) M
inst✝ : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ f (↑c.cast • x) = ↑c.cast • f x

Proof state:
n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₁
inst✝³ : FunLike F M M₁
inst✝² : AddMonoidHomClass F M M₁
inst✝¹ : Module (ZMod n) M
inst✝ : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ f (↑c.cast • x) = ↑c.cast • f x

Tactic:
exact map_intCast_smul f _ _ (cast c) x

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem isBasis_empty_iff (M : Matroid α) : M.IsBasis I ∅ ↔ I = ∅ :=
  ⟨fun h ↦ subset_empty_iff.mp h.subset, fun h ↦ by (rw [h]; exact M.empty_indep.isBasis_self)⟩

Proof state:
α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis ∅ ∅

Tactic:
exact M.empty_indep.isBasis_self

Result:
no goals

Proof state:
α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis I ∅

Tactic:
(rw [h]; exact M.empty_indep.isBasis_self)

Result:
no goals

Proof state:
α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis I ∅

Tactic:
rw [h]

Result:
α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis ∅ ∅
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.div_const {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) :
    Integrable (fun x => f x / c) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : NormedDivisionRing 𝕜
f : α → 𝕜
h : Integrable f μ
c : 𝕜
⊢ Integrable (fun x => f x / c) μ

Tactic:
simp_rw [div_eq_mul_inv, h.mul_const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_swap (a : Vector α n) (i j : Nat) {hi hj} (k : Nat) (hk : k < n) :
    (a.swap i j hi hj)[k] = if k = i then a[j] else if k = j then a[i] else a[k]

Proof state:
case mk
α : Type u_1
n i j : Nat
hi : i < n
hj : j < n
k : Nat
hk : k < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.swap i j hi hj)[k] =
    if k = i then { toArray := toArray✝, size_toArray := size_toArray✝ }[j]
    else
      if k = j then { toArray := toArray✝, size_toArray := size_toArray✝ }[i]
      else { toArray := toArray✝, size_toArray := size_toArray✝ }[k]

Tactic:
simp_all [Array.getElem_swap]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i j : Nat
hi : i < n
hj : j < n
k : Nat
hk : k < n
⊢ (a.swap i j hi hj)[k] = if k = i then a[j] else if k = j then a[i] else a[k]

Tactic:
cases a

Result:
case mk
α : Type u_1
n i j : Nat
hi : i < n
hj : j < n
k : Nat
hk : k < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.swap i j hi hj)[k] =
    if k = i then { toArray := toArray✝, size_toArray := size_toArray✝ }[j]
    else
      if k = j then { toArray := toArray✝, size_toArray := size_toArray✝ }[i]
      else { toArray := toArray✝, size_toArray := size_toArray✝ }[k]
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem lift_σ {X : C} : prod.lift (𝟙 X) 0 ≫ σ = 𝟙 X

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X : C
⊢ prod.lift (𝟙 X) 0 ≫ σ = 𝟙 X

Tactic:
rw [← Category.assoc, IsIso.hom_inv_id]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFac_dvd (n : ℕ) : minFac n ∣ n :=
  if n1 : n = 1 then by simp [n1] else (minFac_has_prop n1).2.1

Proof state:
n : ℕ
n1 : n = 1
⊢ n.minFac ∣ n

Tactic:
simp [n1]

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma min_def (a b : α) : min a b = if a ≤ b then a else b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b = if a ≤ b then a else b

Tactic:
rw [LinearOrder.min_def a]

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

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a⁻¹ < b / c ↔ c < a * b

Tactic:
rw [div_eq_mul_inv, lt_mul_inv_iff_mul_lt, inv_mul_lt_iff_lt_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem lt_rpow_inv_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) : x < y ^ z⁻¹ ↔ x ^z < y

Proof state:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
simp only [← not_le, rpow_inv_le_iff hz]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma IsInducing.of_comp_iff (hg : IsInducing g) : IsInducing (g ∘ f) ↔ IsInducing f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
⊢ IsInducing (g ∘ f) ↔ IsInducing f

Tactic:
refine ⟨fun h ↦ ?_, hg.comp⟩

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
h : IsInducing (g ∘ f)
⊢ IsInducing f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
h : IsInducing (g ∘ f)
⊢ IsInducing f

Tactic:
rw [isInducing_iff, hg.eq_induced, induced_compose, h.eq_induced]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_alter_of_beq [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β}
    (h : k == k') : k' ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : (k == k') = true
⊢ k' ∈ alter m k f ↔ (f (get? m k)).isSome = true

Tactic:
rw [mem_alter, if_pos h]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem zmodEquivTrunc_apply {x : ZMod (p ^ n)} :
    zmodEquivTrunc p n x =
      ZMod.castHom (m := p ^ n) (by rfl) (TruncatedWittVector p n (ZMod p)) x :=
  rfl

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
x : ZMod (p ^ n)
⊢ p ^ n ∣ p ^ n

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem IsCompact.lift'_closure_nhdsSet {K : Set X} (hK : IsCompact K) :
    (𝓝ˢ K).lift' closure = 𝓝ˢ K

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
⊢ U ∈ (𝓝ˢ K).lift' closure

Tactic:
rcases hK.exists_isOpen_closure_subset hU with ⟨V, hVo, hKV, hVU⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
V : Set X
hVo : IsOpen V
hKV : K ⊆ V
hVU : closure V ⊆ U
⊢ U ∈ (𝓝ˢ K).lift' closure

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
V : Set X
hVo : IsOpen V
hKV : K ⊆ V
hVU : closure V ⊆ U
⊢ U ∈ (𝓝ˢ K).lift' closure

Tactic:
exact mem_of_superset (mem_lift' <| hVo.mem_nhdsSet.2 hKV) hVU

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).lift' closure = 𝓝ˢ K

Tactic:
refine le_antisymm (fun U hU ↦ ?_) (le_lift'_closure _)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
⊢ U ∈ (𝓝ˢ K).lift' closure
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_eq_norm_mul_iff {x y : E} :
    ⟪x, y⟫ = (‖x‖ : 𝕜) * ‖y‖ ↔ (‖y‖ : 𝕜) • x = (‖x‖ : 𝕜) • y

Proof state:
case inr.ha
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ ↑‖x‖ ≠ 0

Tactic:
rwa [Ne, ofReal_eq_zero, norm_eq_zero]

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
y : E
⊢ ⟪0, y⟫_𝕜 = ↑‖0‖ * ↑‖y‖ ↔ ↑‖y‖ • 0 = ↑‖0‖ • y

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y

Tactic:
rcases eq_or_ne x 0 with (rfl | h₀)

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
y : E
⊢ ⟪0, y⟫_𝕜 = ↑‖0‖ * ↑‖y‖ ↔ ↑‖y‖ • 0 = ↑‖0‖ • y

case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y

Tactic:
rw [inner_eq_norm_mul_iff_div h₀, div_eq_inv_mul, mul_smul, inv_smul_eq_iff₀]

Result:
case inr.ha
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ ↑‖x‖ ≠ 0
-- Mathlib/Data/Multiset/Powerset.lean
theorem mem_powersetAux {l : List α} {s} : s ∈ powersetAux l ↔ s ≤ ↑l :=
  Quotient.inductionOn s <| by simp [powersetAux_eq_map_coe, Subperm, and_comm]

Proof state:
α : Type u_1
l : List α
s : Multiset α
⊢ ∀ (a : List α), ⟦a⟧ ∈ powersetAux l ↔ ⟦a⟧ ≤ ↑l

Tactic:
simp [powersetAux_eq_map_coe, Subperm, and_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem leftMulMatrix_eq_repr_mul (x : S) (i j) : leftMulMatrix b x i j = b.repr (x * b j) i

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
x : S
i j : m
⊢ (leftMulMatrix b) x i j = (b.repr (x * b j)) i

Tactic:
rw [leftMulMatrix_apply, toMatrix_lmul' b x i j]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem nhdsSet_iUnion {ι : Sort*} (s : ι → Set X) : 𝓝ˢ (⋃ i, s i) = ⨆ i, 𝓝ˢ (s i)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Sort u_3
s : ι → Set X
⊢ 𝓝ˢ (⋃ i, s i) = ⨆ i, 𝓝ˢ (s i)

Tactic:
simp only [nhdsSet, image_iUnion, sSup_iUnion (β := Filter X)]

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_same : ∀ {l : List α}, Forall₂ Rₐ l l ↔ ∀ x ∈ l, Rₐ x x
  | [] => by simp
  | a :: l => by simp [@forall₂_same l]

Proof state:
α : Type u_1
Rₐ : α → α → Prop
a : α
l : List α
⊢ Forall₂ Rₐ (a :: l) (a :: l) ↔ ∀ (x : α), x ∈ a :: l → Rₐ x x

Tactic:
simp [@forall₂_same l]

Result:
no goals

Proof state:
α : Type u_1
Rₐ : α → α → Prop
⊢ Forall₂ Rₐ [] [] ↔ ∀ (x : α), x ∈ [] → Rₐ x x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean
lemma nnnorm_sqrt (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a ^ (1 / 2)‖₊ = ‖a‖₊ ^ (1 / 2)

Tactic:
exact nnnorm_nnrpow a (by norm_num) ha

Result:
no goals

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ 0 < 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖sqrt a‖₊ = NNReal.sqrt ‖a‖₊

Tactic:
rw [sqrt_eq_nnrpow, NNReal.sqrt_eq_rpow]

Result:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a ^ (1 / 2)‖₊ = ‖a‖₊ ^ (1 / 2)
-- Mathlib/Analysis/Calculus/Deriv/ZPow.lean
theorem iter_deriv_inv (k : ℕ) (x : 𝕜) :
    deriv^[k] Inv.inv x = (∏ i ∈ Finset.range k, (-1 - i : 𝕜)) * x ^ (-1 - k : ℤ)

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
k : ℕ
x : 𝕜
⊢ deriv^[k] Inv.inv x = (∏ i ∈ Finset.range k, (-1 - ↑i)) * x ^ (-1 - ↑k)

Tactic:
simpa only [zpow_neg_one, Int.cast_neg, Int.cast_one] using iter_deriv_zpow (-1) x k

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem card_fintypeIoc : Fintype.card (Set.Ioc a b) = b - a

Proof state:
a b : ℕ
⊢ Fintype.card ↑(Set.Ioc a b) = b - a

Tactic:
rw [Fintype.card_ofFinset, card_Ioc]

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem inv_aux : (∀ x, p x ↔ p (f x)) ↔ ∀ x, p x ↔ p (f⁻¹ x) :=
  f⁻¹.surjective.forall.trans <| by simp_rw [f.apply_inv_self, Iff.comm]

Proof state:
α : Type u_4
p : α → Prop
f : Perm α
⊢ (∀ (x : α), p (f⁻¹ x) ↔ p (f (f⁻¹ x))) ↔ ∀ (x : α), p x ↔ p (f⁻¹ x)

Tactic:
simp_rw [f.apply_inv_self, Iff.comm]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_subset_Ioo_right (h : b₁ < b₂) : Ioc a b₁ ⊆ Ioo a b₂

Proof state:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Ioc a b₁ ⊆ Set.Ioo a b₂

Tactic:
exact Set.Ioc_subset_Ioo_right h

Result:
no goals

Proof state:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Ioc a b₁ ⊆ Ioo a b₂

Tactic:
rw [← coe_subset, coe_Ioc, coe_Ioo]

Result:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Ioc a b₁ ⊆ Set.Ioo a b₂
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem T_pow_mul_apply_one (n : ℤ) (g : SL(2, ℤ)) : (T ^ n * g) 1 = g 1

Proof state:
case h
n : ℤ
g : SL(2, ℤ)
j : Fin 2
⊢ ↑(T ^ n * g) 1 j = ↑g 1 j

Tactic:
simp [coe_T_zpow, Matrix.vecMul, dotProduct, Fin.sum_univ_succ, vecTail]

Result:
no goals

Proof state:
n : ℤ
g : SL(2, ℤ)
⊢ ↑(T ^ n * g) 1 = ↑g 1

Tactic:
ext j

Result:
case h
n : ℤ
g : SL(2, ℤ)
j : Fin 2
⊢ ↑(T ^ n * g) 1 j = ↑g 1 j
-- Mathlib/Data/Complex/ExponentialBounds.lean
theorem log_two_lt_d9 : log 2 < 0.6931471808 :=
  lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 log_two_near_10).1) (by norm_num)

Proof state:
⊢ 1 / 10 ^ 10 + 287209 / 414355 < 0.6931471808

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w

Proof state:
w : Nat
⊢ (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w

Tactic:
simp [intMin]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem Eq.congr_right {x y z : α} (h : x = y) : z = x ↔ z = y

Proof state:
α : Sort u_1
x y z : α
h : x = y
⊢ z = x ↔ z = y

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem conjTranspose_row [Star α] (v : m → α) : (row ι v)ᴴ = col ι (star v)

Proof state:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
⊢ (row ι v)ᴴ = col ι (star v)

Tactic:
ext

Result:
case a
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
i✝ : m
j✝ : ι
⊢ (row ι v)ᴴ i✝ j✝ = col ι (star v) i✝ j✝

Proof state:
case a
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
i✝ : m
j✝ : ι
⊢ (row ι v)ᴴ i✝ j✝ = col ι (star v) i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
lemma hasSum_choose_mul_geometric_of_norm_lt_one
    (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
    HasSum (fun n ↦ (n + k).choose k * r ^ n) (1 / (1 - r) ^ (k + 1))

Proof state:
𝕜 : Type u_3
inst✝ : NormedDivisionRing 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ HasSum (fun n => ↑((n + k).choose k) * r ^ n) (1 / (1 - r) ^ (k + 1))

Tactic:
convert hasSum_choose_mul_geometric_of_norm_lt_one' k hr

Result:
case h.e'_6
𝕜 : Type u_3
inst✝ : NormedDivisionRing 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ 1 / (1 - r) ^ (k + 1) = Ring.inverse (1 - r) ^ (k + 1)

Proof state:
case h.e'_6
𝕜 : Type u_3
inst✝ : NormedDivisionRing 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ 1 / (1 - r) ^ (k + 1) = Ring.inverse (1 - r) ^ (k + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem left_inv_eq_left_inv (h : B * A = 1) (g : C * A = 1) : B = C

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : B * A = 1
g : C * A = 1
⊢ B = C

Tactic:
rw [← inv_eq_left_inv h, ← inv_eq_left_inv g]

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_iInf {f : α → β} {x : Filter α} {y : ι → Filter β} :
    Tendsto f x (⨅ i, y i) ↔ ∀ i, Tendsto f x (y i)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : α → β
x : Filter α
y : ι → Filter β
⊢ Tendsto f x (⨅ i, y i) ↔ ∀ (i : ι), Tendsto f x (y i)

Tactic:
simp only [Tendsto, le_iInf_iff]

Result:
no goals
-- Mathlib/Control/Traversable/Lemmas.lean
theorem traverse_map' (g : α → β) (h : β → G γ) :
    traverse (h ∘ g) = (traverse h ∘ map g : t α → G (t γ))

Proof state:
case h
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
x✝ : t α
⊢ traverse (h ∘ g) x✝ = (traverse h ∘ map g) x✝

Tactic:
rw [comp_apply, traverse_map]

Result:
no goals

Proof state:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
⊢ traverse (h ∘ g) = traverse h ∘ map g

Tactic:
ext

Result:
case h
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
x✝ : t α
⊢ traverse (h ∘ g) x✝ = (traverse h ∘ map g) x✝
-- Mathlib/Order/Directed.lean
theorem exists_lt_of_directed_ge [IsDirected β (· ≥ ·)] :
    ∃ a b : β, a < b

Proof state:
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
⊢ ∃ a b, a < b

Tactic:
rcases exists_pair_ne β with ⟨a, b, hne⟩

Result:
case intro.intro
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
a b : β
hne : a ≠ b
⊢ ∃ a b, a < b

Proof state:
case intro.intro.inl
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
a b : β
hne : a ≠ b
ha : IsBot a
⊢ ∃ a b, a < b

case intro.intro.inr.intro
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
a b : β
hne : a ≠ b
c : β
hc : c < a
⊢ ∃ a b, a < b

Tactic:
exacts [⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩]

Result:
no goals

Proof state:
case intro.intro
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
a b : β
hne : a ≠ b
⊢ ∃ a b, a < b

Tactic:
rcases isBot_or_exists_lt a with (ha | ⟨c, hc⟩)

Result:
case intro.intro.inl
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
a b : β
hne : a ≠ b
ha : IsBot a
⊢ ∃ a b, a < b

case intro.intro.inr.intro
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
a b : β
hne : a ≠ b
c : β
hc : c < a
⊢ ∃ a b, a < b
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem inv {x y} (h : c x y) : c x⁻¹ y⁻¹ :=
  c.map_of_mul_left_rel_one Inv.inv (fun x => by simp only [inv_mul_cancel, c.refl 1]) h

Proof state:
M : Type u_1
inst✝ : Group M
c : Con M
x✝ y : M
h : c x✝ y
x : M
⊢ c (x⁻¹ * x) 1

Tactic:
simp only [inv_mul_cancel, c.refl 1]

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_eq_matrix_trace (f : M →ₗ[R] M) :
    trace R M f = Matrix.trace (LinearMap.toMatrix b b f)

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
⊢ (trace R M) f = ((toMatrix b b) f).trace

Tactic:
classical
rw [trace_eq_matrix_trace_of_finset R b.reindexFinsetRange, ← traceAux_def, ← traceAux_def,
  traceAux_eq R b b.reindexFinsetRange]

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
⊢ (trace R M) f = ((toMatrix b b) f).trace

Tactic:
rw [trace_eq_matrix_trace_of_finset R b.reindexFinsetRange, ← traceAux_def, ← traceAux_def,
  traceAux_eq R b b.reindexFinsetRange]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[simp] lemma reProdIm_eq_empty : s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅

Proof state:
s t : Set ℝ
⊢ s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty, reProdIm_nonempty, -not_and, not_and_or]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
lemma CompleteSpace.snd_of_prod [UniformSpace β] [CompleteSpace (α × β)] [h : Nonempty α] :
    CompleteSpace β where
  complete hf :=
    let ⟨x⟩ := h
    let ⟨(a, b), hab⟩ := CompleteSpace.complete <| (cauchy_pure (a := x)).prod hf
    ⟨b, by simpa only [map_snd_prod, nhds_prod_eq] using map_mono (m := Prod.snd) hab⟩

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace (α × β)
h : Nonempty α
f✝ : Filter β
hf : Cauchy f✝
x a : α
b : β
hab : pure x ×ˢ f✝ ≤ 𝓝 (a, b)
⊢ f✝ ≤ 𝓝 b

Tactic:
simpa only [map_snd_prod, nhds_prod_eq] using map_mono (m := Prod.snd) hab

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma evalEval_C (x y : R) (p : R[X]) : (C p).evalEval x y = p.eval x

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ evalEval x y (C p) = eval x p

Tactic:
rw [evalEval, eval_C]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_union_left [DecidableEq α] : image₂ f (s ∪ s') t = image₂ f s t ∪ image₂ f s' t :=
  coe_injective <| by
    push_cast
    exact image2_union_left

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ ↑(image₂ f (s ∪ s') t) = ↑(image₂ f s t ∪ image₂ f s' t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ image2 f (↑s ∪ ↑s') ↑t = image2 f ↑s ↑t ∪ image2 f ↑s' ↑t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ image2 f (↑s ∪ ↑s') ↑t = image2 f ↑s ↑t ∪ image2 f ↑s' ↑t

Tactic:
exact image2_union_left

Result:
no goals