harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma F_int_eq_of_mem_Icc (k : ℕ) {a : ℝ} (ha : a ∈ Icc 0 1) {t : ℝ} (ht : 0 < t) :
    F_int k a t = (F_nat k a t) + (F_nat k (1 - a) t)

Proof state:
case h.e'_2.h.e'_5.h
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
n : ℤ
⊢ f_int k a t n = Int.rec (f_nat k a t) (f_nat k (1 - a) t) n

Tactic:
cases n

Result:
case h.e'_2.h.e'_5.h.ofNat
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.ofNat a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a✝)

case h.e'_2.h.e'_5.h.negSucc
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.negSucc a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.negSucc a✝)

Proof state:
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
⊢ ∑' (n : ℤ), f_int k a t n = ∑' (n : ℕ), f_nat k a t n + ∑' (n : ℕ), f_nat k (1 - a) t n

Tactic:
convert ((summable_f_nat k a ht).hasSum.int_rec (summable_f_nat k (1 - a) ht).hasSum).tsum_eq
  using 3 with n

Result:
case h.e'_2.h.e'_5.h
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
n : ℤ
⊢ f_int k a t n = Int.rec (f_nat k a t) (f_nat k (1 - a) t) n

Proof state:
case h.e'_2.h.e'_5.h.ofNat
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.ofNat a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a✝)

Tactic:
rw [f_int_ofNat _ ha.1]

Result:
no goals

Proof state:
case h.e'_2.h.e'_5.h.negSucc
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.negSucc a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.negSucc a✝)

Tactic:
rw [f_int_negSucc _ ha.2]

Result:
no goals

Proof state:
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
⊢ F_int k (↑a) t = F_nat k a t + F_nat k (1 - a) t

Tactic:
simp only [F_int, F_nat, Function.Periodic.lift_coe]

Result:
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
⊢ ∑' (n : ℤ), f_int k a t n = ∑' (n : ℕ), f_nat k a t n + ∑' (n : ℕ), f_nat k (1 - a) t n
-- Mathlib/Order/SupClosed.lean
lemma SupClosed.sSup_mem (hs : SupClosed s) (ht : t.Finite) (hbot : ⊥ ∈ s) (hts : t ⊆ s) :
    sSup t ∈ s

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
⊢ sSup t ∈ s

Tactic:
have := ht.to_subtype

Result:
α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite ↑t
⊢ sSup t ∈ s

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite ↑t
⊢ ⨆ a, ↑a ∈ s

Tactic:
exact hs.iSup_mem hbot (by simpa)

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite ↑t
⊢ ∀ (i : ↑t), ↑i ∈ s

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite ↑t
⊢ sSup t ∈ s

Tactic:
rw [sSup_eq_iSup']

Result:
α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite ↑t
⊢ ⨆ a, ↑a ∈ s
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem preAleph_nat (n : ℕ) : preAleph n = n

Proof state:
n : ℕ
⊢ preAleph ↑n = ↑n

Tactic:
rw [← card_preOmega, preOmega_natCast, card_nat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : List α) :
    (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l l' : List α
⊢ List.foldlM f b (l ++ l') = do
    let init ← List.foldlM f b l
    List.foldlM f init l'

Tactic:
induction l generalizing b <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Basic.lean
lemma Even.pow_nonneg (hn : Even n) (a : R) : 0 ≤ a ^ n

Proof state:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ (k + k)

Tactic:
rw [pow_add]

Result:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ k * a ^ k

Proof state:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ k * a ^ k

Tactic:
exact mul_self_nonneg _

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Even n
a : R
⊢ 0 ≤ a ^ n

Tactic:
obtain ⟨k, rfl⟩ := hn

Result:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
a : R
k : ℕ
⊢ 0 ≤ a ^ (k + k)
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem localTriv_coordChange_eq {b : B} (hb : b ∈ Z.baseSet i ∩ Z.baseSet j) (v : F) :
    (Z.localTriv i).coordChangeL R (Z.localTriv j) b v = Z.coordChange i j b v

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet j
v : F
⊢ (Trivialization.coordChangeL R (Z.localTriv i) (Z.localTriv j) b) v = (Z.coordChange i j b) v

Tactic:
rw [Trivialization.coordChangeL_apply', localTriv_symm_fst, localTriv_apply, coordChange_comp]

Result:
case a
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet j
v : F
⊢ { proj := (b, v).1, snd := (Z.coordChange i (Z.indexAt (b, v).1) (b, v).1) (b, v).2 }.proj ∈
    Z.baseSet i ∩
        Z.baseSet
          (Z.indexAt { proj := (b, v).1, snd := (Z.coordChange i (Z.indexAt (b, v).1) (b, v).1) (b, v).2 }.proj) ∩
      Z.baseSet j

case hb
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet j
v : F
⊢ b ∈ (Z.localTriv i).baseSet ∩ (Z.localTriv j).baseSet

Proof state:
case a
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet j
v : F
⊢ { proj := (b, v).1, snd := (Z.coordChange i (Z.indexAt (b, v).1) (b, v).1) (b, v).2 }.proj ∈
    Z.baseSet i ∩
        Z.baseSet
          (Z.indexAt { proj := (b, v).1, snd := (Z.coordChange i (Z.indexAt (b, v).1) (b, v).1) (b, v).2 }.proj) ∩
      Z.baseSet j

case hb
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i j : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet j
v : F
⊢ b ∈ (Z.localTriv i).baseSet ∩ (Z.localTriv j).baseSet

Tactic:
exacts [⟨⟨hb.1, Z.mem_baseSet_at b⟩, hb.2⟩, hb]

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem isIso_inv_app (α : F ⟶ G) {_ : IsIso α} (X) : (inv α).app X = inv (α.app X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
x✝ : IsIso α
X : C
⊢ (inv α).app X = inv (α.app X)

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Result:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
x✝ : IsIso α
X : C
⊢ α.app X ≫ (inv α).app X = 𝟙 (F.obj X)

Proof state:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
x✝ : IsIso α
X : C
⊢ α.app X ≫ (inv α).app X = 𝟙 (F.obj X)

Tactic:
rw [← NatTrans.comp_app]

Result:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
x✝ : IsIso α
X : C
⊢ (α ≫ inv α).app X = 𝟙 (F.obj X)

Proof state:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
x✝ : IsIso α
X : C
⊢ (α ≫ inv α).app X = 𝟙 (F.obj X)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem getElem?_eraseIdx_of_ge (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : i ≤ j) :
    (l.eraseIdx i)[j]? = l[j + 1]?

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : i ≤ j
⊢ (l.eraseIdx i h)[j]? = l[j + 1]?

Tactic:
rw [getElem?_eraseIdx]

Result:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : i ≤ j
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j + 1]?

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : i ≤ j
⊢ j < i → l[j]? = l[j + 1]?

Tactic:
intro h'

Result:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h'✝ : i ≤ j
h' : j < i
⊢ l[j]? = l[j + 1]?

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h'✝ : i ≤ j
h' : j < i
⊢ l[j]? = l[j + 1]?

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : i ≤ j
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j + 1]?

Tactic:
simp only [dite_eq_ite, ite_eq_right_iff]

Result:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : i ≤ j
⊢ j < i → l[j]? = l[j + 1]?
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem lift_lt_aleph1 {c : Cardinal.{u}} : lift.{v} c < ℵ₁ ↔ c < ℵ₁

Proof state:
c : Cardinal.{u}
⊢ lift.{v, u} c < ℵ_ 1 ↔ c < ℵ_ 1

Tactic:
simpa using lift_lt (b := ℵ₁)

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_apply_right (a : α) : toIocMod hp a (a + p) = a + p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIocMod hp a (a + p) = a + p

Tactic:
rw [toIocMod_eq_iff hp, Set.right_mem_Ioc]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ z, a + p = a + p + z • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ z, a + p = a + p + z • p

Tactic:
exact ⟨lt_add_of_pos_right _ hp, 0, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p = a + p + 0 • p

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
/-- `μ.sigmaFiniteSetWRT' ν` has maximal `ν`-measure among all measurable sets `s` with sigma-finite
`μ.restrict s`. -/
lemma measure_sigmaFiniteSetWRT' (μ ν : Measure α) [IsFiniteMeasure ν] :
    ν (μ.sigmaFiniteSetWRT' ν)
      = ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ν (μ.sigmaFiniteSetWRT' ν) = ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ν (μ.sigmaFiniteSetWRT' ν) ≤ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν (μ.sigmaFiniteSetWRT' ν)

Proof state:
case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))), ν (μ.sigmaFiniteSetWRT' ν) ≤
    ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

Tactic:
exact le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) (μ.sigmaFiniteSetWRT' ν)
  measurableSet_sigmaFiniteSetWRT'

Result:
no goals

Proof state:
case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν (μ.sigmaFiniteSetWRT' ν)

Tactic:
exact le_of_tendsto' (tendsto_measure_sigmaFiniteSetGE μ ν)
  (fun _ ↦ measure_mono (Set.subset_iUnion _ _))

Result:
no goals

Proof state:
case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ν (μ.sigmaFiniteSetWRT' ν) ≤ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

Tactic:
refine (le_iSup (f := fun _ ↦ _)
  (sigmaFinite_restrict_sigmaFiniteSetWRT' μ ν)).trans ?_

Result:
case a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ ⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))), ν (μ.sigmaFiniteSetWRT' ν) ≤
    ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s
-- Mathlib/Data/Nat/Squarefree.lean
lemma primeFactors_prod (hs : ∀ p ∈ s, p.Prime) : primeFactors (∏ p ∈ s, p) = s

Proof state:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
⊢ (∏ p ∈ s, p).primeFactors = s

Tactic:
have hn : ∏ p ∈ s, p ≠ 0 := prod_ne_zero_iff.2 fun p hp ↦ (hs _ hp).ne_zero

Result:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
⊢ (∏ p ∈ s, p).primeFactors = s

Proof state:
case h
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
⊢ p ∈ (∏ p ∈ s, p).primeFactors ↔ p ∈ s

Tactic:
rw [mem_primeFactors_of_ne_zero hn, and_congr_right (fun hp ↦ hp.prime.dvd_finset_prod_iff _)]

Result:
case h
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
⊢ (Prime p ∧ ∃ a ∈ s, p ∣ a) ↔ p ∈ s

Proof state:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
⊢ (∏ p ∈ s, p).primeFactors = s

Tactic:
ext p

Result:
case h
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
⊢ p ∈ (∏ p ∈ s, p).primeFactors ↔ p ∈ s

Proof state:
case h
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
⊢ (Prime p ∧ ∃ a ∈ s, p ∣ a) ↔ p ∈ s

Tactic:
refine ⟨?_, fun hp ↦ ⟨hs _ hp, _, hp, dvd_rfl⟩⟩

Result:
case h
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
⊢ (Prime p ∧ ∃ a ∈ s, p ∣ a) → p ∈ s

Proof state:
case h.intro.intro.intro
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ s
hpq : p ∣ q
⊢ p ∈ s

Tactic:
rwa [← ((hs _ hq).dvd_iff_eq hp.ne_one).1 hpq]

Result:
no goals

Proof state:
case h
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
⊢ (Prime p ∧ ∃ a ∈ s, p ∣ a) → p ∈ s

Tactic:
rintro ⟨hp, q, hq, hpq⟩

Result:
case h.intro.intro.intro
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ s
hpq : p ∣ q
⊢ p ∈ s
-- Mathlib/RingTheory/Complex.lean
theorem Algebra.trace_complex_apply (z : ℂ) : Algebra.trace ℝ ℂ z = 2 * z.re

Proof state:
z : ℂ
⊢ (trace ℝ ℂ) z = 2 * z.re

Tactic:
rw [Algebra.trace_eq_matrix_trace Complex.basisOneI, Algebra.leftMulMatrix_complex,
  Matrix.trace_fin_two]

Result:
z : ℂ
⊢ !![z.re, -z.im; z.im, z.re] 0 0 + !![z.re, -z.im; z.im, z.re] 1 1 = 2 * z.re

Proof state:
z : ℂ
⊢ !![z.re, -z.im; z.im, z.re] 0 0 + !![z.re, -z.im; z.im, z.re] 1 1 = 2 * z.re

Tactic:
exact (two_mul _).symm

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem proj_clift : proj (T.clift (e, γ) i) = γ i

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : LocallyCompactPair ι ↑T.baseSet
γ : C(ι, ↑T.baseSet)
i : ι
e : ↑T.source
⊢ proj ↑((T.clift (e, γ)) i) = ↑(γ i)

Tactic:
simp [clift, liftCM, proj_lift]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem length_eq_lengthTR : @List.length = @List.lengthTR

Proof state:
case h.h
α : Type u_1
⊢ ∀ (x : List α), x.length = x.lengthTR

Tactic:
intro as

Result:
case h.h
α : Type u_1
as : List α
⊢ as.length = as.lengthTR

Proof state:
case h
α : Type u_1
⊢ length = lengthTR

Tactic:
apply funext

Result:
case h.h
α : Type u_1
⊢ ∀ (x : List α), x.length = x.lengthTR

Proof state:
case h

⊢ ∀ (x : Type u_1), length = lengthTR

Tactic:
intro α

Result:
case h
α : Type u_1
⊢ length = lengthTR

Proof state:
⊢ @length = @lengthTR

Tactic:
apply funext

Result:
case h

⊢ ∀ (x : Type u_1), length = lengthTR

Proof state:
case h.h
α : Type u_1
as : List α
⊢ as.length = as.lengthTR

Tactic:
simp [lengthTR, ← length_add_eq_lengthTRAux]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv (h : S.RightHomologyData) :
    h.rightHomologyIso.hom ≫ h.homologyIso.inv = S.rightHomologyIso.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ h.rightHomologyIso.hom ≫ (S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).inv = S.rightHomologyIso.hom

Tactic:
simp only [Iso.trans_inv, Iso.symm_inv, Iso.hom_inv_id_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ h.rightHomologyIso.hom ≫ h.homologyIso.inv = S.rightHomologyIso.hom

Tactic:
dsimp only [homologyIso]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ h.rightHomologyIso.hom ≫ (S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).inv = S.rightHomologyIso.hom
-- Mathlib/Algebra/Group/Invertible/Basic.lean
theorem Commute.invOf_right [Monoid α] {a b : α} [Invertible b] (h : Commute a b) :
    Commute a (⅟ b) :=
  calc
    a * ⅟ b = ⅟ b * (b * a * ⅟ b)

Proof state:
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute a b
⊢ a * ⅟b = ⅟b * (b * a * ⅟b)

Tactic:
simp [mul_assoc]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute a b
⊢ ⅟b * (b * a * ⅟b) = ⅟b * (a * b * ⅟b)

Tactic:
rw [h.eq]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute a b
⊢ ⅟b * (a * b * ⅟b) = ⅟b * a

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/Topology/Order/ExtendFrom.lean
theorem eq_lim_at_left_extendFrom_Ioo [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α]
    [OrderTopology α] [TopologicalSpace β] [T2Space β] {f : α → β} {a b : α} {la : β} (hab : a < b)
    (ha : Tendsto f (𝓝[>] a) (𝓝 la)) : extendFrom (Ioo a b) f a = la

Proof state:
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ a ∈ Icc a b

Tactic:
simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc]

Result:
no goals

Proof state:
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ Tendsto f (𝓝[Ioo a b] a) (𝓝 la)

Tactic:
simpa [hab]

Result:
no goals

Proof state:
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ a ∈ closure (Ioo a b)

Tactic:
rw [closure_Ioo hab.ne]

Result:
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ a ∈ Icc a b

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ extendFrom (Ioo a b) f a = la

Tactic:
apply extendFrom_eq

Result:
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ a ∈ closure (Ioo a b)

case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ Tendsto f (𝓝[Ioo a b] a) (𝓝 la)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attachWith_some {x : α} {P : α → Prop} (h : ∀ (b : α), b ∈ some x → P b) :
    (some x).attachWith P h = some ⟨x, by simpa using h⟩ := rfl

Proof state:
α : Type ?u.796
x : α
P : α → Prop
h : ∀ (b : α), b ∈ some x → P b
⊢ P x

Tactic:
simpa using h

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem isFractional_of_le_one (I : Submodule R P) (h : I ≤ 1) : IsFractional S I

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
⊢ IsFractional S I

Tactic:
use 1, S.one_mem

Result:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
⊢ ∀ b ∈ I, IsInteger R (1 • b)

Proof state:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R b

Tactic:
obtain ⟨b', b'_mem, rfl⟩ := mem_one.mp (h hb)

Result:
case right.intro.refl
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b' : R
hb : (algebraMap R P) b' ∈ I
⊢ IsInteger R ((algebraMap R P) b')

Proof state:
case right.intro.refl
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b' : R
hb : (algebraMap R P) b' ∈ I
⊢ IsInteger R ((algebraMap R P) b')

Tactic:
exact Set.mem_range_self b'

Result:
no goals

Proof state:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
⊢ ∀ b ∈ I, IsInteger R (1 • b)

Tactic:
intro b hb

Result:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R (1 • b)

Proof state:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R (1 • b)

Tactic:
rw [one_smul]

Result:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R b