harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Nilpotent/Exp.lean
theorem exp_zero_eq_one : exp (0 : A) = 1

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
h₁ : ∑ i ∈ range 1, (↑i !)⁻¹ • 0 ^ i = exp 0
⊢ exp 0 = 1

Tactic:
rw [range_one, sum_singleton, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero,
  one_smul] at h₁

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
h₁ : 1 = exp 0
⊢ exp 0 = 1

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
⊢ exp 0 = 1

Tactic:
have h₁ := exp_eq_truncated (pow_one (0 : A))

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
h₁ : ∑ i ∈ range 1, (↑i !)⁻¹ • 0 ^ i = exp 0
⊢ exp 0 = 1

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
h₁ : 1 = exp 0
⊢ exp 0 = 1

Tactic:
exact h₁.symm

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
/-- A function from a locally finite preorder is monotone if and only if it is monotone when
restricted to pairs satisfying `a ⩿ b`. -/
lemma monotone_iff_forall_wcovBy [Preorder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : Monotone f ↔ ∀ a b : α, a ⩿ b → f a ≤ f b

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ (a b : α), a ⩿ b → f a ≤ f b

Tactic:
refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩

Result:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⩿ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b
-- Mathlib/Order/Filter/AtTopBot/Ring.lean
theorem not_tendsto_pow_atTop_atBot [LinearOrderedRing α] :
    ∀ {n : ℕ}, ¬Tendsto (fun x : α => x ^ n) atTop atBot
  | 0 => by simp [not_tendsto_const_atBot]
  | n + 1 => (tendsto_pow_atTop n.succ_ne_zero).not_tendsto disjoint_atTop_atBot

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
⊢ ¬Tendsto (fun x => x ^ 0) atTop atBot

Tactic:
simp [not_tendsto_const_atBot]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem FiniteDimensional.nonempty_linearEquiv_of_finrank_eq
    [Module.Finite R M] [Module.Finite R M'] (cond : finrank R M = finrank R M') :
    Nonempty (M ≃ₗ[R] M') :=
  nonempty_linearEquiv_of_lift_rank_eq <| by simp only [← finrank_eq_rank, cond, lift_natCast]

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : Free R M'
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
cond : finrank R M = finrank R M'
⊢ lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')

Tactic:
simp only [← finrank_eq_rank, cond, lift_natCast]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.spectrum_one_eq [Nontrivial A] :
    spectrum R (1 : A) = {1}

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
this : 1 = (algebraMap R A) 1
⊢ spectrum R 1 = {1}

Tactic:
rw [this, spectrum_algebraMap_eq]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
⊢ spectrum R 1 = {1}

Tactic:
have : (1 : A) = algebraMap R A 1 := Eq.symm (RingHom.map_one (algebraMap R A))

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
this : 1 = (algebraMap R A) 1
⊢ spectrum R 1 = {1}
-- Mathlib/Analysis/Complex/RealDeriv.lean
theorem HasDerivAt.complexToReal_fderiv {f : ℂ → ℂ} {f' x : ℂ} (h : HasDerivAt f f' x) :
    HasFDerivAt f (f' • (1 : ℂ →L[ℝ] ℂ)) x

Proof state:
f : ℂ → ℂ
f' x : ℂ
h : HasDerivAt f f' x
⊢ HasFDerivAt f (f' • 1) x

Tactic:
simpa only [Complex.restrictScalars_one_smulRight] using h.hasFDerivAt.restrictScalars ℝ

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem toComplex_eq_zero {x : ℤ[i]} : (x : ℂ) = 0 ↔ x = 0

Proof state:
x : ℤ[i]
⊢ toComplex x = 0 ↔ x = 0

Tactic:
rw [← toComplex_zero, toComplex_inj]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma one_mem_inv_mul_iff : (1 : α) ∈ t⁻¹ * s ↔ ¬Disjoint s t

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s t : Finset α
⊢ 1 ∈ t⁻¹ * s ↔ ¬Disjoint s t

Tactic:
aesop (add simp [not_disjoint_iff_nonempty_inter, mem_mul, mul_eq_one_iff_eq_inv,
  Finset.Nonempty])

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma exists_not_orthogonal_self (v : ℙ F (m → F)) : ∃ w, ¬ orthogonal w v

Proof state:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : ℙ F (m → F)
⊢ ∃ w, ¬v.orthogonal w

Tactic:
exact exists_not_self_orthogonal v

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : ℙ F (m → F)
⊢ ∃ w, ¬w.orthogonal v

Tactic:
simp only [orthogonal_comm]

Result:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : ℙ F (m → F)
⊢ ∃ w, ¬v.orthogonal w
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem preservesEpimorphsisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
    PreservesEpimorphisms F :=
  { preserves := fun {X} {Y} f hf =>
      ⟨by
        intro Z g h H
        replace H := congr_arg (adj.homEquiv X Z) H
        rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi,
          Equiv.apply_eq_iff_eq] at H⟩ }

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
⊢ ∀ {Z : D} (g h : F.obj Y ⟶ Z), F.map f ≫ g = F.map f ≫ h → g = h

Tactic:
intro Z g h H

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : F.map f ≫ g = F.map f ≫ h
⊢ g = h

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : (adj.homEquiv X Z) (F.map f ≫ g) = (adj.homEquiv X Z) (F.map f ≫ h)
⊢ g = h

Tactic:
rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi,
  Equiv.apply_eq_iff_eq] at H

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : F.map f ≫ g = F.map f ≫ h
⊢ g = h

Tactic:
replace H := congr_arg (adj.homEquiv X Z) H

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : (adj.homEquiv X Z) (F.map f ≫ g) = (adj.homEquiv X Z) (F.map f ≫ h)
⊢ g = h
-- Mathlib/Topology/Homotopy/HSpaces.lean
theorem delayReflLeft_one (γ : Path x y) : delayReflLeft 1 γ = γ

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflLeft 1 γ = γ

Tactic:
simp only [delayReflLeft, delayReflRight_one, Path.symm_symm]

Result:
no goals
-- Mathlib/Logic/Nontrivial/Basic.lean
theorem Function.Injective.exists_ne [Nontrivial α] {f : α → β}
    (hf : Function.Injective f) (y : β) : ∃ x, f x ≠ y

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : f x₂ = y
⊢ ∃ x, f x ≠ y

Tactic:
exact ⟨x₁, (hf.ne_iff' h).2 hx⟩

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : ¬f x₂ = y
⊢ ∃ x, f x ≠ y

Tactic:
exact ⟨x₂, h⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
⊢ ∃ x, f x ≠ y

Tactic:
rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
⊢ ∃ x, f x ≠ y

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
⊢ ∃ x, f x ≠ y

Tactic:
by_cases h : f x₂ = y

Result:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : f x₂ = y
⊢ ∃ x, f x ≠ y

case neg
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : ¬f x₂ = y
⊢ ∃ x, f x ≠ y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} :
    l.toArray.pmap f H = (l.pmap f (by simpa using H)).toArray

Proof state:
α : Type ?u.1531
β : Type ?u.1588
l : List α
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l.toArray → P a
⊢ ∀ (a : α), a ∈ l → P a

Tactic:
simpa using H

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l.toArray → P a
⊢ pmap f l.toArray H = (List.pmap f l ⋯).toArray

Tactic:
simp [pmap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/SOM.lean
theorem Poly.append_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁ ++ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx

Proof state:
ctx : Context
p₁ p₂ : Poly
⊢ denote ctx ([] ++ p₂) = denote ctx [] + denote ctx p₂

Tactic:
simp!

Result:
no goals

Proof state:
ctx : Context
p₁✝ p₂ : Poly
v : Nat × Mon
p₁ : List (Nat × Mon)
⊢ denote ctx (v :: p₁ ++ p₂) = denote ctx (v :: p₁) + denote ctx p₂

Tactic:
simp! [append_denote _ p₁ p₂, Nat.add_assoc]

Result:
no goals

Proof state:
ctx : Context
p₁ p₂ : Poly
⊢ denote ctx (p₁ ++ p₂) = denote ctx p₁ + denote ctx p₂

Tactic:
match p₁ with
| [] => simp!
| v :: p₁ => simp! [append_denote _ p₁ p₂, Nat.add_assoc]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma mul_ne_bot (a b : EReal) :
    a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Proof state:
a b : EReal
⊢ a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
rw [ne_eq, mul_eq_bot]

Result:
a b : EReal
⊢ ¬(a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Proof state:
a b : EReal
⊢ ¬(a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
set_option push_neg.use_distrib true in push_neg

Result:
a b : EReal
⊢ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Proof state:
a b : EReal
⊢ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
rfl

Result:
no goals

Proof state:
a b : EReal
⊢ ¬(a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
push_neg

Result:
a b : EReal
⊢ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem Monotone.cauchySeq_alternating_series_of_tendsto_zero (hfa : Monotone f)
    (hf0 : Tendsto f atTop (𝓝 0)) : CauchySeq fun n ↦ ∑ i ∈ range n, (-1) ^ i * f i

Proof state:
f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i

Tactic:
simp_rw [mul_comm]

Result:
f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ x ∈ Finset.range n, f x * (-1) ^ x

Proof state:
f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ x ∈ Finset.range n, f x * (-1) ^ x

Tactic:
exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_subset_sups : s ○ t ⊆ s ⊻ t

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ s ○ t ⊆ s ⊻ t

Tactic:
simp_rw [subset_iff, mem_sups, mem_disjSups]

Result:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ ∀ ⦃x : α⦄, (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ ∀ ⦃x : α⦄, (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x

Tactic:
exact fun c ⟨a, b, ha, hb, _, hc⟩ => ⟨a, b, ha, hb, hc⟩

Result:
no goals
-- Mathlib/Data/Nat/BitIndices.lean
theorem bitIndices_sorted {n : ℕ} : n.bitIndices.Sorted (· < ·)

Proof state:
n : ℕ
⊢ Sorted (fun x1 x2 => x1 < x2) n.bitIndices

Tactic:
induction' n using binaryRec with b n hs

Result:
case z

⊢ Sorted (fun x1 x2 => x1 < x2) (bitIndices 0)

case f
b : Bool
n : ℕ
hs : Sorted (fun x1 x2 => x1 < x2) n.bitIndices
⊢ Sorted (fun x1 x2 => x1 < x2) (bit b n).bitIndices

Proof state:
case f
b : Bool
n : ℕ
hs : Sorted (fun x1 x2 => x1 < x2) n.bitIndices
⊢ List.Pairwise (fun a b => a < b) n.bitIndices

Tactic:
exact List.Pairwise.imp (by simp) hs

Result:
no goals

Proof state:
b : Bool
n : ℕ
hs : Sorted (fun x1 x2 => x1 < x2) n.bitIndices
⊢ ∀ {a b : ℕ}, a < b → a < b

Tactic:
simp

Result:
no goals

Proof state:
case z

⊢ Sorted (fun x1 x2 => x1 < x2) (bitIndices 0)

Tactic:
simp

Result:
no goals

Proof state:
case f
b : Bool
n : ℕ
hs : Sorted (fun x1 x2 => x1 < x2) n.bitIndices
⊢ Sorted (fun x1 x2 => x1 < x2) (bit b n).bitIndices

Tactic:
suffices List.Pairwise (fun a b ↦ a < b) n.bitIndices by
  cases b <;> simpa [List.Sorted, bit_false, bit_true, List.pairwise_map]

Result:
case f
b : Bool
n : ℕ
hs : Sorted (fun x1 x2 => x1 < x2) n.bitIndices
⊢ List.Pairwise (fun a b => a < b) n.bitIndices

Proof state:
b : Bool
n : ℕ
hs : Sorted (fun x1 x2 => x1 < x2) n.bitIndices
this : List.Pairwise (fun a b => a < b) n.bitIndices
⊢ Sorted (fun x1 x2 => x1 < x2) (bit b n).bitIndices

Tactic:
cases b <;> simpa [List.Sorted, bit_false, bit_true, List.pairwise_map]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle (x - y) x = Real.arcsin (‖y‖ / ‖x - y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle (x - y) x = ↑(Real.arcsin (‖y‖ / ‖x - y‖))

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle x (x - y) = ↑(Real.arcsin (‖y‖ / ‖x - y‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle x (x - y) = ↑(Real.arcsin (‖y‖ / ‖x - y‖))

Tactic:
exact (-o).oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem unique_single_eq_iff [Unique α] {b' : M} : single a b = single a' b' ↔ b = b'

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Unique α
b' : M
⊢ single a b = single a' b' ↔ b = b'

Tactic:
rw [Finsupp.unique_ext_iff, Unique.eq_default a, Unique.eq_default a', single_eq_same,
  single_eq_same]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem baseChange_zero : baseChange A (0 : M →ₗ[R] N) = 0

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ baseChange A 0 = 0

Tactic:
ext

Result:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A 0)) 1) x✝ = ((AlgebraTensorModule.curry 0) 1) x✝

Proof state:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A 0)) 1) x✝ = ((AlgebraTensorModule.curry 0) 1) x✝

Tactic:
simp [baseChange_eq_ltensor]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem setLaverage_congr (h : s =ᵐ[μ] t) : ⨍⁻ x in s, f x ∂μ = ⨍⁻ x in t, f x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
h : s =ᶠ[ae μ] t
⊢ ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in t, f x ∂μ

Tactic:
simp only [setLaverage_eq, setLIntegral_congr h, measure_congr h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem setIfInBounds_comm (a b : α)
    {i j : Nat} (as : Array α) (h : i ≠ j) :
    (as.setIfInBounds i a).setIfInBounds j b = (as.setIfInBounds j b).setIfInBounds i a

Proof state:
case mk
α : Type u_1
a b : α
i j : Nat
h : i ≠ j
toList✝ : List α
⊢ ({ toList := toList✝ }.setIfInBounds i a).setIfInBounds j b =
    ({ toList := toList✝ }.setIfInBounds j b).setIfInBounds i a

Tactic:
simp [List.set_comm _ _ _ h]

Result:
no goals

Proof state:
α : Type u_1
a b : α
i j : Nat
as : Array α
h : i ≠ j
⊢ (as.setIfInBounds i a).setIfInBounds j b = (as.setIfInBounds j b).setIfInBounds i a

Tactic:
cases as

Result:
case mk
α : Type u_1
a b : α
i j : Nat
h : i ≠ j
toList✝ : List α
⊢ ({ toList := toList✝ }.setIfInBounds i a).setIfInBounds j b =
    ({ toList := toList✝ }.setIfInBounds j b).setIfInBounds i a
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_const_of_isProbabilityMeasure (c : ε) (hq_pos : 0 < q) [IsProbabilityMeasure μ] :
    eLpNorm' (fun _ : α => c) q μ = ‖c‖ₑ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
c : ε
hq_pos : 0 < q
inst✝ : IsProbabilityMeasure μ
⊢ eLpNorm' (fun x => c) q μ = ‖c‖ₑ

Tactic:
simp [eLpNorm'_const c hq_pos, measure_univ]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
/-- Note: the "obvious" statement `(piCongrLeft' P e).symm g a = g (e a)` doesn't typecheck: the
LHS would have type `P a` while the RHS would have type `P (e.symm (e a))`. This lemma is a way
around it in the case where `a` is of the form `e.symm b`, so we can use `g b` instead of
`g (e (e.symm b))`. -/
@[simp]
lemma piCongrLeft'_symm_apply_apply (P : α → Sort*) (e : α ≃ β) (g : ∀ b, P (e.symm b)) (b : β) :
    (piCongrLeft' P e).symm g (e.symm b) = g b

Proof state:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ HEq (g (e (e.symm b))) (g b)

Tactic:
exact congr_arg_heq _ (e.apply_symm_apply _)

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ (piCongrLeft' P e).symm g (e.symm b) = g b

Tactic:
rw [piCongrLeft'_symm_apply, ← heq_iff_eq, rec_heq_iff_heq]

Result:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ HEq (g (e (e.symm b))) (g b)
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualDistrib_dualDistribInvOfBasis_right_inverse (b : Basis ι R M) (c : Basis κ R N) :
    comp (dualDistribInvOfBasis b c) (dualDistrib R M N) = LinearMap.id

Proof state:
case mk
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∑ x : ι, ∑ x_1 : κ, ((Finsupp.single x 1) i * (Finsupp.single x_1 1) j) • b.coord x ⊗ₜ[R] c.coord x_1 =
    b.coord i ⊗ₜ[R] c.coord j

Tactic:
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]

Result:
case mk
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ((Finsupp.single i 1) i * (Finsupp.single j 1) j) • b.coord i ⊗ₜ[R] c.coord j = b.coord i ⊗ₜ[R] c.coord j

case mk.h₀
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ b_1 ∈ Finset.univ, b_1 ≠ j → ((Finsupp.single i 1) i * (Finsupp.single b_1 1) j) • b.coord i ⊗ₜ[R] c.coord b_1 = 0

case mk.h₁
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ j ∉ Finset.univ → ((Finsupp.single i 1) i * (Finsupp.single j 1) j) • b.coord i ⊗ₜ[R] c.coord j = 0

case mk.h₀
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ i → ∑ x : κ, ((Finsupp.single b_1 1) i * (Finsupp.single x 1) j) • b.coord b_1 ⊗ₜ[R] c.coord x = 0

case mk.h₁
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ i ∉ Finset.univ → ∑ x : κ, ((Finsupp.single i 1) i * (Finsupp.single x 1) j) • b.coord i ⊗ₜ[R] c.coord x = 0
-- Mathlib/LinearAlgebra/Matrix/Permutation.lean
theorem det_permutation [CommRing R] : det (σ.permMatrix R) = Perm.sign σ

Proof state:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : CommRing R
⊢ (Perm.permMatrix R σ).det = ↑↑(Perm.sign σ)

Tactic:
rw [← Matrix.mul_one (σ.permMatrix R), PEquiv.toMatrix_toPEquiv_mul,
  det_permute, det_one, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_and {x y : BitVec w} :
    (x &&& y).setWidth k = x.setWidth k &&& y.setWidth k

Proof state:
w k : Nat
x y : BitVec w
⊢ setWidth k (x &&& y) = setWidth k x &&& setWidth k y

Tactic:
ext i h

Result:
case pred
w k : Nat
x y : BitVec w
i : Nat
h : i < k
⊢ (setWidth k (x &&& y)).getLsbD i = (setWidth k x &&& setWidth k y).getLsbD i

Proof state:
case pred
w k : Nat
x y : BitVec w
i : Nat
h : i < k
⊢ (setWidth k (x &&& y)).getLsbD i = (setWidth k x &&& setWidth k y).getLsbD i

Tactic:
simp [h]

Result:
no goals