harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_id (l : Vector (Vector α m) n) : l.flatMap id = l.flatten

Proof state:
α : Type u_1
m n : Nat
l : Vector (Vector α m) n
⊢ l.flatMap id = l.flatten

Tactic:
simp [flatMap_def]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_two_mul : sinh (2 * x) = 2 * sinh x * cosh x

Proof state:
x : ℝ
⊢ sinh (2 * x) = 2 * sinh x * cosh x

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(sinh (2 * x)) = ↑(2 * sinh x * cosh x)

Proof state:
x : ℝ
⊢ ↑(sinh (2 * x)) = ↑(2 * sinh x * cosh x)

Tactic:
simp [sinh_two_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_eq_append_iff {a b c d : List α} :
    a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b

Proof state:
case cons
α : Type u_1
b d : List α
a : α
as : List α
ih : ∀ {c : List α}, as ++ b = c ++ d ↔ (∃ a', c = as ++ a' ∧ b = a' ++ d) ∨ ∃ c', as = c ++ c' ∧ d = c' ++ b
c : List α
⊢ a :: as ++ b = c ++ d ↔ (∃ a', c = a :: as ++ a' ∧ b = a' ++ d) ∨ ∃ c', a :: as = c ++ c' ∧ d = c' ++ b

Tactic:
cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]

Result:
no goals

Proof state:
α : Type u_1
a b c d : List α
⊢ a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b

Tactic:
induction a generalizing c with
| nil => simp_all
| cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]

Result:
no goals

Proof state:
case nil
α : Type u_1
b d c : List α
⊢ [] ++ b = c ++ d ↔ (∃ a', c = [] ++ a' ∧ b = a' ++ d) ∨ ∃ c', [] = c ++ c' ∧ d = c' ++ b

Tactic:
simp_all

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem HasFDerivAt.hasFDerivAt_norm_smul_neg
    (ht : t < 0) (h : HasFDerivAt (‖·‖) f x) :
    HasFDerivAt (‖·‖) (-f) (t • x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t < 0
h : HasFDerivAt (fun x => ‖x‖) f x
⊢ HasFDerivAt (fun x => ‖x‖) (-f) (t • x)

Tactic:
simpa [ht] using h.hasFDerivAt_norm_smul ht.ne

Result:
no goals
-- Mathlib/CategoryTheory/Endofunctor/Algebra.lean
theorem right_inv : A.str ≫ strInv h = 𝟙 _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ F.map ((h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)

Tactic:
congr

Result:
case e_a
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ (h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str = 𝟙 A.a

Proof state:
case e_a
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ (h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str = 𝟙 A.a

Tactic:
exact left_inv h

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ A.str ≫ strInv h = 𝟙 (F.obj A.a)

Tactic:
rw [strInv, ← (h.to ⟨F.obj A.1, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]

Result:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ F.map ((h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsBigO.smul (h₁ : k₁ =O[l] k₂) (h₂ : f' =O[l] g') :
    (fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : f' =O[l] g'
⊢ (fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x

Tactic:
obtain ⟨c₁, h₁⟩ := h₁.isBigOWith

Result:
case intro
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁✝ : k₁ =O[l] k₂
h₂ : f' =O[l] g'
c₁ : ℝ
h₁ : IsBigOWith c₁ l k₁ k₂
⊢ (fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x

Proof state:
case intro
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁✝ : k₁ =O[l] k₂
h₂ : f' =O[l] g'
c₁ : ℝ
h₁ : IsBigOWith c₁ l k₁ k₂
⊢ (fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x

Tactic:
obtain ⟨c₂, h₂⟩ := h₂.isBigOWith

Result:
case intro.intro
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁✝ : k₁ =O[l] k₂
h₂✝ : f' =O[l] g'
c₁ : ℝ
h₁ : IsBigOWith c₁ l k₁ k₂
c₂ : ℝ
h₂ : IsBigOWith c₂ l f' g'
⊢ (fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x

Proof state:
case intro.intro
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : BoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : BoundedSMul 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁✝ : k₁ =O[l] k₂
h₂✝ : f' =O[l] g'
c₁ : ℝ
h₁ : IsBigOWith c₁ l k₁ k₂
c₂ : ℝ
h₂ : IsBigOWith c₂ l f' g'
⊢ (fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x

Tactic:
exact (h₁.smul h₂).isBigO

Result:
no goals
-- Mathlib/Data/Finsupp/ToDFinsupp.lean
theorem toDFinsupp_support (f : ι →₀ M) : f.toDFinsupp.support = f.support

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
⊢ f.toDFinsupp.support = f.support

Tactic:
ext

Result:
case h
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
a✝ : ι
⊢ a✝ ∈ f.toDFinsupp.support ↔ a✝ ∈ f.support

Proof state:
case h
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
a✝ : ι
⊢ a✝ ∈ f.toDFinsupp.support ↔ a✝ ∈ f.support

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem HasGradientAt.hasDerivAt (h : HasGradientAt g g' u) :
    HasDerivAt g (starRingEnd 𝕜 g') u

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasGradientAt g g' u
⊢ HasDerivAt g ((starRingEnd 𝕜) g') u

Tactic:
rw [hasGradientAt_iff_hasFDerivAt, hasFDerivAt_iff_hasDerivAt] at h

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g (((toDual 𝕜 𝕜) g') 1) u
⊢ HasDerivAt g ((starRingEnd 𝕜) g') u

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g (((toDual 𝕜 𝕜) g') 1) u
⊢ HasDerivAt g ((starRingEnd 𝕜) g') u

Tactic:
simpa using h

Result:
no goals
-- Mathlib/RingTheory/Support.lean
lemma Module.annihilator_le_of_mem_support (hp : p ∈ Module.support R M) :
    Module.annihilator R M ≤ p.asIdeal

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
hp : p ∈ support R M
⊢ annihilator R M ≤ p.asIdeal

Tactic:
obtain ⟨m, hm⟩ := mem_support_iff_exists_annihilator.mp hp

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
hp : p ∈ support R M
m : M
hm : (Submodule.span R {m}).annihilator ≤ p.asIdeal
⊢ annihilator R M ≤ p.asIdeal

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
hp : p ∈ support R M
m : M
hm : (Submodule.span R {m}).annihilator ≤ p.asIdeal
⊢ annihilator R M ≤ p.asIdeal

Tactic:
exact le_trans ((Submodule.subtype _).annihilator_le_of_injective Subtype.val_injective) hm

Result:
no goals
-- Mathlib/Algebra/Regular/SMul.lean
theorem pow (n : ℕ) (ra : IsSMulRegular M a) : IsSMulRegular M (a ^ n)

Proof state:
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ n)

Tactic:
induction n with
| zero => rw [pow_zero]; simp only [one]
| succ n hn =>
  rw [pow_succ']
  exact (ra.smul_iff (a ^ n)).mpr hn

Result:
no goals

Proof state:
case succ
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a * a ^ n)

Tactic:
exact (ra.smul_iff (a ^ n)).mpr hn

Result:
no goals

Proof state:
case zero
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ 0)

Tactic:
rw [pow_zero]

Result:
case zero
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M 1

Proof state:
case succ
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a ^ (n + 1))

Tactic:
rw [pow_succ']

Result:
case succ
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a * a ^ n)

Proof state:
case zero
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M 1

Tactic:
simp only [one]

Result:
no goals
-- Mathlib/Data/Multiset/Functor.lean
theorem naturality {G H : Type _ → Type _} [Applicative G] [Applicative H] [CommApplicative G]
    [CommApplicative H] (eta : ApplicativeTransformation G H) {α β : Type _} (f : α → G β)
    (x : Multiset α) : eta (traverse f x) = traverse (@eta _ ∘ f) x

Proof state:
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ ∀ (a : List α), (fun {α} => eta.app α) (traverse f ⟦a⟧) = traverse ((fun {α} => eta.app α) ∘ f) ⟦a⟧

Tactic:
intro

Result:
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
a✝ : List α
⊢ (fun {α} => eta.app α) (traverse f ⟦a✝⟧) = traverse ((fun {α} => eta.app α) ∘ f) ⟦a✝⟧

Proof state:
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ (fun {α} => eta.app α) (traverse f x) = traverse ((fun {α} => eta.app α) ∘ f) x

Tactic:
refine Quotient.inductionOn x ?_

Result:
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ ∀ (a : List α), (fun {α} => eta.app α) (traverse f ⟦a⟧) = traverse ((fun {α} => eta.app α) ∘ f) ⟦a⟧

Proof state:
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
a✝ : List α
⊢ (fun {α} => eta.app α) (traverse f ⟦a✝⟧) = traverse ((fun {α} => eta.app α) ∘ f) ⟦a✝⟧

Tactic:
simp only [quot_mk_to_coe, traverse, lift_coe, Function.comp_apply,
  ApplicativeTransformation.preserves_map, LawfulTraversable.naturality]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
/-- An alternate spelling of `term_def` for the case `f 0 = 0`. -/
lemma term_def₀ {f : ℕ → ℂ} (hf : f 0 = 0) (s : ℂ) (n : ℕ) :
    LSeries.term f s n = f n * (n : ℂ) ^ (- s)

Proof state:
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
⊢ term f s n = f n * ↑n ^ (-s)

Tactic:
rw [LSeries.term]

Result:
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
⊢ (if n = 0 then 0 else f n / ↑n ^ s) = f n * ↑n ^ (-s)

Proof state:
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
⊢ (if n = 0 then 0 else f n / ↑n ^ s) = f n * ↑n ^ (-s)

Tactic:
split_ifs with h <;> simp [h, hf, cpow_neg, div_eq_inv_mul, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_xor {x y : BitVec w} :
    (x ^^^ y).msb = (x.msb ^^ y.msb)

Proof state:
w : Nat
x y : BitVec w
⊢ (x ^^^ y).msb = (x.msb ^^ y.msb)

Tactic:
simp [BitVec.msb]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Basic.lean
theorem cokernelCoforkOfCofork_ofπ {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
    cokernelCoforkOfCofork (Cofork.ofπ π w) = CokernelCofork.ofπ π (by simp [w]) :=
  rfl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (f - g) ≫ π = 0

Tactic:
simp [w]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt

Proof state:
b : Bool
⊢ (ofBool b).toInt = -b.toInt

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.isBasis_subset (hI : M.IsBasis I X) (hIY : I ⊆ Y) (hYX : Y ⊆ X) :
    M.IsBasis I Y

Proof state:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J

Tactic:
exact fun J hJ hIJ hJY ↦ hI.eq_of_subset_indep hJ hIJ (hJY.trans hYX)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ M.IsBasis I Y

Tactic:
rw [isBasis_iff (hYX.trans hI.subset_ground), and_iff_right hI.indep, and_iff_right hIY]

Result:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J
-- Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
theorem homotopyEquiv_inv_ι {X : C} (I J : InjectiveResolution X) :
    J.ι ≫ (homotopyEquiv I J).inv = I.ι

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ J.ι ≫ (I.homotopyEquiv J).inv = I.ι

Tactic:
simp [homotopyEquiv]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem zip_inits_tails (s : Stream' α) : zip appendStream' (inits s) (tails s) = const s

Proof state:
case a
α : Type u
s : Stream' α
n : ℕ
⊢ (zip appendStream' s.inits s.tails).get n = (const s).get n

Tactic:
rw [get_zip, get_inits, get_tails, get_const, take_succ, cons_append_stream, append_take_drop,
  Stream'.eta]

Result:
no goals

Proof state:
α : Type u
s : Stream' α
⊢ zip appendStream' s.inits s.tails = const s

Tactic:
apply Stream'.ext

Result:
case a
α : Type u
s : Stream' α
⊢ ∀ (n : ℕ), (zip appendStream' s.inits s.tails).get n = (const s).get n

Proof state:
case a
α : Type u
s : Stream' α
⊢ ∀ (n : ℕ), (zip appendStream' s.inits s.tails).get n = (const s).get n

Tactic:
intro n

Result:
case a
α : Type u
s : Stream' α
n : ℕ
⊢ (zip appendStream' s.inits s.tails).get n = (const s).get n
-- Mathlib/Data/Complex/Basic.lean
@[simp] lemma div_natCast_im (z : ℂ) (n : ℕ) : (z / n).im = z.im / n

Proof state:
z : ℂ
n : ℕ
⊢ (z / ↑n).im = z.im / ↑n

Tactic:
rw [div_natCast]

Result:
no goals
-- Mathlib/Data/NNReal/Basic.lean
theorem iSup_mul (f : ι → ℝ≥0) (a : ℝ≥0) : (⨆ i, f i) * a = ⨆ i, f i * a

Proof state:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ ⨆ i, a * f i = ⨆ i, f i * a

Tactic:
simp_rw [mul_comm]

Result:
no goals

Proof state:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ i, f i) * a = ⨆ i, f i * a

Tactic:
rw [mul_comm, mul_iSup]

Result:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ ⨆ i, a * f i = ⨆ i, f i * a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_xor {x : BitVec w} : 0#w ^^^ x = x

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (0#w ^^^ x).getLsbD i = x.getLsbD i

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ 0#w ^^^ x = x

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (0#w ^^^ x).getLsbD i = x.getLsbD i
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_iff_isIso_rightHomologyMap' (φ : S₁ ⟶ S₂)
    (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
    QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)

Tactic:
rw [γ.quasiIso_iff, γ.rightHomologyMap'_eq]

Result:
no goals

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default

Result:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)
-- Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean
lemma shortExact_iff_degreewise_shortExact :
    S.ShortExact ↔ ∀ (i : ι), (S.map (eval C c i)).ShortExact

Proof state:
case mpr
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ (∀ (i : ι), (S.map (eval C c i)).ShortExact) → S.ShortExact

Tactic:
exact shortExact_of_degreewise_shortExact S

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.ShortExact ↔ ∀ (i : ι), (S.map (eval C c i)).ShortExact

Tactic:
constructor

Result:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.ShortExact → ∀ (i : ι), (S.map (eval C c i)).ShortExact

case mpr
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ (∀ (i : ι), (S.map (eval C c i)).ShortExact) → S.ShortExact

Proof state:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.ShortExact → ∀ (i : ι), (S.map (eval C c i)).ShortExact

Tactic:
intro hS i

Result:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
⊢ (S.map (eval C c i)).ShortExact

Proof state:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
this✝ : Mono S.f
this : Epi S.g
⊢ (S.map (eval C c i)).ShortExact

Tactic:
exact hS.map (eval C c i)

Result:
no goals

Proof state:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
this : Mono S.f
⊢ (S.map (eval C c i)).ShortExact

Tactic:
have := hS.epi_g

Result:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
this✝ : Mono S.f
this : Epi S.g
⊢ (S.map (eval C c i)).ShortExact

Proof state:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
⊢ (S.map (eval C c i)).ShortExact

Tactic:
have := hS.mono_f

Result:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
this : Mono S.f
⊢ (S.map (eval C c i)).ShortExact
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Nodup.perm {l l' : List α} (hR : l.Nodup) (hl : l ~ l') : l'.Nodup :=
  Pairwise.perm hR hl (by intro x y h h'; simp_all)

Proof state:
α : Type u_1
l l' : List α
hR : l.Nodup
hl : l ~ l'
x y : α
h : x ≠ y
h' : y = x
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l l' : List α
hR : l.Nodup
hl : l ~ l'
⊢ ∀ {x y : α}, x ≠ y → y ≠ x

Tactic:
intro x y h h'

Result:
α : Type u_1
l l' : List α
hR : l.Nodup
hl : l ~ l'
x y : α
h : x ≠ y
h' : y = x
⊢ False
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem _root_.AlternatingMap.measure_parallelepiped (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ)
    (v : Fin n → G) : ω.measure (parallelepiped v) = ENNReal.ofReal |ω v|

Proof state:
G : Type u_3
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
v : Fin n → G
⊢ ω.measure (parallelepiped v) = ENNReal.ofReal |(ω ⇑(finBasisOfFinrankEq ℝ G ⋯) • (finBasisOfFinrankEq ℝ G ⋯).det) v|

Tactic:
simp only [addHaar_parallelepiped, AlternatingMap.measure, coe_nnreal_smul_apply,
  AlternatingMap.smul_apply, Algebra.id.smul_eq_mul, abs_mul, ENNReal.ofReal_mul (abs_nonneg _),
  ← Real.enorm_eq_ofReal_abs, enorm]

Result:
no goals

Proof state:
G : Type u_3
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
v : Fin n → G
⊢ ω.measure (parallelepiped v) = ENNReal.ofReal |ω v|

Tactic:
conv_rhs => rw [ω.eq_smul_basis_det (finBasisOfFinrankEq ℝ G _i.out)]

Result:
G : Type u_3
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
v : Fin n → G
⊢ ω.measure (parallelepiped v) = ENNReal.ofReal |(ω ⇑(finBasisOfFinrankEq ℝ G ⋯) • (finBasisOfFinrankEq ℝ G ⋯).det) v|
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem of_basis_mul {κ ι : Type*} (m : Basis κ R M) (n : Basis ι R N)
    (H : LinearIndependent R fun (i : κ × ι) ↦ (m i.1).1 * (n i.2).1) : M.LinearDisjoint N

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis κ R ↥M
n : Basis ι R ↥N
H : LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)
⊢ M.LinearDisjoint N

Tactic:
rw [LinearIndependent] at H

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis κ R ↥M
n : Basis ι R ↥N
H : Function.Injective ⇑(Finsupp.linearCombination R fun i => ↑(m i.1) * ↑(n i.2))
⊢ M.LinearDisjoint N

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis κ R ↥M
n : Basis ι R ↥N
H : Function.Injective ⇑(Finsupp.linearCombination R fun i => ↑(m i.1) * ↑(n i.2))
⊢ M.LinearDisjoint N

Tactic:
exact of_basis_mul' M N m n H

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_iff_ne_none : o.isSome ↔ o ≠ none

Proof state:
α✝ : Type u_1
o : Option α✝
⊢ o.isSome = true ↔ o ≠ none

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_smul_const_vsub_eq_neg_weightedVSub (w : ι → k) (p₂ : ι → P) (p₁ : P)
    (h : ∑ i ∈ s, w i = 0) : (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = -s.weightedVSub p₂ w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₂ : ι → P
p₁ : P
h : ∑ i ∈ s, w i = 0
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = -(s.weightedVSub p₂) w

Tactic:
rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, zero_sub]

Result:
no goals