harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Lemmas.lean
theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m

Proof state:
n : UInt32
m : Nat
h : m < size
⊢ n < ofNat m → n.toNat < m

Tactic:
simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVec.lean
theorem get_out_bound (s : RefVec aig len) (idx : Nat) (alt : Ref aig) (hidx : len ≤ idx) :
    s.getD idx alt = alt

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : idx < len
⊢ s.get idx h✝ = alt

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
⊢ (if hidx : idx < len then s.get idx hidx else alt) = alt

Tactic:
split

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : idx < len
⊢ s.get idx h✝ = alt

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
⊢ s.getD idx alt = alt

Tactic:
unfold getD

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
⊢ (if hidx : idx < len then s.get idx hidx else alt) = alt

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_eval_neg_coe_nat_of_lt {n k : ℕ} (h : k < n) :
    (ascPochhammer R n).eval (-(k : R)) = 0

Proof state:
case succ.inr.inr
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : n < k
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

Tactic:
omega

Result:
no goals

Proof state:
case succ.inl
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : k < n
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

Tactic:
simp [ih hkn]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
⊢ eval (-↑k) (ascPochhammer R (n + 1)) = 0

Tactic:
rw [ascPochhammer_succ_eval]

Result:
case succ
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

Proof state:
case succ.inr.inl
R : Type u
inst✝ : Ring R
k : ℕ
ih : k < k → eval (-↑k) (ascPochhammer R k) = 0
h : k < k + 1
⊢ eval (-↑k) (ascPochhammer R k) * (-↑k + ↑k) = 0

Tactic:
simp

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Ring R
k : ℕ
h : k < 0
⊢ eval (-↑k) (ascPochhammer R 0) = 0

Tactic:
contradiction

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

Tactic:
rcases lt_trichotomy k n with hkn | rfl | hkn

Result:
case succ.inl
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : k < n
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

case succ.inr.inl
R : Type u
inst✝ : Ring R
k : ℕ
ih : k < k → eval (-↑k) (ascPochhammer R k) = 0
h : k < k + 1
⊢ eval (-↑k) (ascPochhammer R k) * (-↑k + ↑k) = 0

case succ.inr.inr
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : n < k
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem det_eval_matrixOfPolynomials_eq_det_vandermonde {n : ℕ} (v : Fin n → R) (p : Fin n → R[X])
    (h_deg : ∀ i, (p i).natDegree = i) (h_monic : ∀ i, Monic <| p i) :
    (Matrix.vandermonde v).det = (Matrix.of (fun i j => ((p j).eval (v i)))).det

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i
h_monic : ∀ (i : Fin n), (p i).Monic
⊢ (vandermonde v).det = (of fun i j => eval (v i) (p j)).det

Tactic:
rw [Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials v p (fun i ↦
    Nat.le_of_eq (h_deg i)), Matrix.det_mul,
    Matrix.det_matrixOfPolynomials p h_deg h_monic, mul_one]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem IsDedekindDomain.exists_forall_sub_mem_ideal {ι : Type*} {s : Finset ι} (P : ι → Ideal R)
    (e : ι → ℕ) (prime : ∀ i ∈ s, Prime (P i))
    (coprime : ∀ᵉ (i ∈ s) (j ∈ s), i ≠ j → P i ≠ P j) (x : s → R) :
    ∃ y, ∀ (i) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
x : { x // x ∈ s } → R
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i

Tactic:
obtain ⟨y, hy⟩ :=
  IsDedekindDomain.exists_representative_mod_finset P e prime coprime fun i =>
    Ideal.Quotient.mk _ (x i)

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
x : { x // x ∈ s } → R
y : R
hy :
  ∀ (i : ι) (hi : i ∈ s), (Ideal.Quotient.mk (P i ^ e i)) y = (Ideal.Quotient.mk (P ↑⟨i, hi⟩ ^ e ↑⟨i, hi⟩)) (x ⟨i, hi⟩)
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
x : { x // x ∈ s } → R
y : R
hy :
  ∀ (i : ι) (hi : i ∈ s), (Ideal.Quotient.mk (P i ^ e i)) y = (Ideal.Quotient.mk (P ↑⟨i, hi⟩ ^ e ↑⟨i, hi⟩)) (x ⟨i, hi⟩)
⊢ ∃ y, ∀ (i : ι) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i

Tactic:
exact ⟨y, fun i hi => Ideal.Quotient.eq.mp (hy i hi)⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_eq_zero_iff (x : ℝ) : log⁺ x = 0 ↔ |x| ≤ 1

Proof state:
x : ℝ
⊢ log⁺ x = 0 ↔ |x| ≤ 1

Tactic:
rw [← posLog_abs, ← log_nonpos_iff (abs_nonneg x)]

Result:
x : ℝ
⊢ log⁺ |x| = 0 ↔ log |x| ≤ 0

Proof state:
x : ℝ
⊢ log⁺ |x| = 0 ↔ log |x| ≤ 0

Tactic:
simp [posLog]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem AffineIndependent.affineSpan_disjoint_of_disjoint [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) {s1 s2 : Set ι} (hd : Disjoint s1 s2) :
    Disjoint (affineSpan k (p '' s1) : Set P) (affineSpan k (p '' s2))

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
hd : Disjoint s1 s2
⊢ Disjoint ↑(affineSpan k (p '' s1)) ↑(affineSpan k (p '' s2))

Tactic:
refine Set.disjoint_left.2 fun p0 hp0s1 hp0s2 => ?_

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
hd : Disjoint s1 s2
p0 : P
hp0s1 : p0 ∈ ↑(affineSpan k (p '' s1))
hp0s2 : p0 ∈ ↑(affineSpan k (p '' s2))
⊢ False

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
hd : Disjoint s1 s2
p0 : P
hp0s1 : p0 ∈ ↑(affineSpan k (p '' s1))
hp0s2 : p0 ∈ ↑(affineSpan k (p '' s2))
⊢ False

Tactic:
obtain ⟨i, hi⟩ := ha.exists_mem_inter_of_exists_mem_inter_affineSpan hp0s1 hp0s2

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
hd : Disjoint s1 s2
p0 : P
hp0s1 : p0 ∈ ↑(affineSpan k (p '' s1))
hp0s2 : p0 ∈ ↑(affineSpan k (p '' s2))
i : ι
hi : i ∈ s1 ∩ s2
⊢ False

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
hd : Disjoint s1 s2
p0 : P
hp0s1 : p0 ∈ ↑(affineSpan k (p '' s1))
hp0s2 : p0 ∈ ↑(affineSpan k (p '' s2))
i : ι
hi : i ∈ s1 ∩ s2
⊢ False

Tactic:
exact Set.disjoint_iff.1 hd hi

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
    (l : Array α) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
toList✝ : List α
f : (a : α) → a ∈ { toList := toList✝ } → β → m γ
g : (a : α) → a ∈ { toList := toList✝ } → β → γ → β
⊢ (forIn' { toList := toList✝ } init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
      init { toList := toList✝ }.attach

Tactic:
simp [List.foldlM_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
f : (a : α) → a ∈ l → β → m γ
g : (a : α) → a ∈ l → β → γ → β
init : β
⊢ (forIn' l init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
      init l.attach

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
toList✝ : List α
f : (a : α) → a ∈ { toList := toList✝ } → β → m γ
g : (a : α) → a ∈ { toList := toList✝ } → β → γ → β
⊢ (forIn' { toList := toList✝ } init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
      init { toList := toList✝ }.attach
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_polynomial (q : R[X]) (a : A) (ha : p a

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
q : R[X]
a : A
ha : autoParam (p a) _auto✝
⊢ cfc (fun a => Polynomial.eval a q) a = (aeval a) q

Tactic:
rw [cfc_map_polynomial .., cfc_id' ..]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_comp_rev {α} (i : Fin (n + 1)) (x : α) (p : Fin n → α) :
    (Fin.insertNth i x p) ∘ Fin.rev = Fin.insertNth (Fin.rev i) x (p ∘ Fin.rev)

Proof state:
case h
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x✝ : α
p : Fin n → α
x : Fin (n + 1)
⊢ (i.insertNth x✝ p ∘ rev) x = i.rev.insertNth x✝ (p ∘ rev) x

Tactic:
apply insertNth_rev

Result:
no goals

Proof state:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x : α
p : Fin n → α
⊢ i.insertNth x p ∘ rev = i.rev.insertNth x (p ∘ rev)

Tactic:
funext x

Result:
case h
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x✝ : α
p : Fin n → α
x : Fin (n + 1)
⊢ (i.insertNth x✝ p ∘ rev) x = i.rev.insertNth x✝ (p ∘ rev) x
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem closure_range_algebraMap : Subfield.closure (Set.range (algebraMap A K)) = ⊤ :=
  top_unique fun z _ ↦ by
    obtain ⟨_, _, -, rfl⟩ := div_surjective (A := A) z
    apply div_mem <;> exact Subfield.subset_closure ⟨_, rfl⟩

Proof state:
case intro.intro.intro
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
w✝¹ w✝ : A
x✝ : (algebraMap A K) w✝¹ / (algebraMap A K) w✝ ∈ ⊤
⊢ (algebraMap A K) w✝¹ / (algebraMap A K) w✝ ∈ Subfield.closure (Set.range ⇑(algebraMap A K))

Tactic:
apply div_mem <;> exact Subfield.subset_closure ⟨_, rfl⟩

Result:
no goals

Proof state:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
z : K
x✝ : z ∈ ⊤
⊢ z ∈ Subfield.closure (Set.range ⇑(algebraMap A K))

Tactic:
obtain ⟨_, _, -, rfl⟩ := div_surjective (A := A) z

Result:
case intro.intro.intro
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
w✝¹ w✝ : A
x✝ : (algebraMap A K) w✝¹ / (algebraMap A K) w✝ ∈ ⊤
⊢ (algebraMap A K) w✝¹ / (algebraMap A K) w✝ ∈ Subfield.closure (Set.range ⇑(algebraMap A K))
-- Mathlib/Data/List/Chain.lean
theorem Chain.induction (p : α → Prop) (l : List α) (h : Chain r a l)
    (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) : ∀ i ∈ l, p i

Proof state:
case nil
α : Type u
r : α → α → Prop
a : α
p : α → Prop
l : List α
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
a✝ : α
initial : p a✝
⊢ ∀ (i : α), i ∈ [] → p i

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
r : α → α → Prop
a✝¹ : α
p : α → Prop
l : List α
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
a b : α
t : List α
hab : r a b
a✝ : Chain r b t
h_ind : p b → ∀ (i : α), i ∈ t → p i
initial : p a
⊢ p b ∧ ∀ (a : α), a ∈ t → p a

Tactic:
exact ⟨carries hab initial, h_ind (carries hab initial)⟩

Result:
no goals

Proof state:
case cons
α : Type u
r : α → α → Prop
a✝¹ : α
p : α → Prop
l : List α
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
a b : α
t : List α
hab : r a b
a✝ : Chain r b t
h_ind : p b → ∀ (i : α), i ∈ t → p i
initial : p a
⊢ ∀ (i : α), i ∈ b :: t → p i

Tactic:
simp only [mem_cons, forall_eq_or_imp]

Result:
case cons
α : Type u
r : α → α → Prop
a✝¹ : α
p : α → Prop
l : List α
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
a b : α
t : List α
hab : r a b
a✝ : Chain r b t
h_ind : p b → ∀ (i : α), i ∈ t → p i
initial : p a
⊢ p b ∧ ∀ (a : α), a ∈ t → p a

Proof state:
α : Type u
r : α → α → Prop
a : α
p : α → Prop
l : List α
h : Chain r a l
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : p a
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
induction h with
| nil => simp
| @cons a b t hab _ h_ind =>
  simp only [mem_cons, forall_eq_or_imp]
  exact ⟨carries hab initial, h_ind (carries hab initial)⟩

Result:
no goals
-- Mathlib/Topology/Homotopy/Basic.lean
theorem equivalence : Equivalence fun f g : C(X, Y) => HomotopicRel f g S :=
  ⟨refl, by apply symm, by apply trans⟩

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set X
⊢ ∀ {x y z : C(X, Y)}, x.HomotopicRel y S → y.HomotopicRel z S → x.HomotopicRel z S

Tactic:
apply trans

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set X
⊢ ∀ {x y : C(X, Y)}, x.HomotopicRel y S → y.HomotopicRel x S

Tactic:
apply symm

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/PID.lean
theorem FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top {R A : Type*}
    [CommRing R] [CommRing A] [Algebra R A] {S : Submonoid R} [IsLocalization S A]
    (I : (FractionalIdeal S A)ˣ) {v : A} (hv : v ∈ (↑I⁻¹ : FractionalIdeal S A))
    (h : Submodule.comap (Algebra.linearMap R A) ((I : Submodule R A) * Submodule.span R {v}) = ⊤) :
    Submodule.IsPrincipal (I : Submodule R A)

Proof state:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}

Tactic:
apply Submodule.map_comap_eq_self

Result:
case h
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑↑I * ↑↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ ↑↑I * Submodule.span R {v} ≤ LinearMap.range (Algebra.linearMap R A)

Proof state:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
h : Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v}) = ⊤
hinv : ↑I * ↑I⁻¹ = 1
⊢ (↑↑I).IsPrincipal

Tactic:
set J := Submodule.comap (Algebra.linearMap R A) ((I : Submodule R A) * Submodule.span R {v})

Result:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
I : (FractionalIdeal S A)ˣ
v : A
hv : v ∈ ↑I⁻¹
hinv : ↑I * ↑I⁻¹ = 1
J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})
h : J = ⊤
⊢ (↑↑I).IsPrincipal
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem SeqRight.monotone_seqRight [LawfulMonad m] (f : γ → m α) (g : γ → m β)
  (hmono₁ : monotone g) (hmono₂ : monotone f) :
    monotone (fun x => g x *> f x)

Proof state:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => g x *> f x

Tactic:
simp only [seqRight_eq]

Result:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => Function.const β id <$> g x <*> f x

Proof state:
case hmono₁.hmono
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone g

Tactic:
assumption

Result:
no goals

Proof state:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => Function.const β id <$> g x <*> f x

Tactic:
apply Seq.monotone_seq

Result:
case hmono₁
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => Function.const β id <$> g x

case hmono₂
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone f

Proof state:
case hmono₂
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone f

Tactic:
assumption

Result:
no goals

Proof state:
case hmono₁
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => Function.const β id <$> g x

Tactic:
apply Functor.monotone_map

Result:
case hmono₁.hmono
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m β
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone g
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_exp_mul_complex {c : ℂ} (hc : c ≠ 0) :
    (∫ x in a..b, Complex.exp (c * x)) = (Complex.exp (c * b) - Complex.exp (c * a)) / c

Proof state:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x) * c / c) x

Tactic:
apply ((Complex.hasDerivAt_exp _).comp x _).div_const c

Result:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun x => c * ↑x) c x

Proof state:
a b : ℝ
c : ℂ
hc : c ≠ 0
⊢ ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x

Tactic:
intro x

Result:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x

Proof state:
a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c

Tactic:
rw [integral_deriv_eq_sub' _ (funext fun x => (D x).deriv) fun x _ => (D x).differentiableAt]

Result:
a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ Complex.exp (c * ↑b) / c - Complex.exp (c * ↑a) / c = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c

a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ ContinuousOn (fun x => Complex.exp (c * ↑x)) [[a, b]]

Proof state:
a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ Complex.exp (c * ↑b) / c - Complex.exp (c * ↑a) / c = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c

Tactic:
ring

Result:
no goals

Proof state:
a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ ContinuousOn (fun x => Complex.exp (c * ↑x)) [[a, b]]

Tactic:
fun_prop

Result:
no goals

Proof state:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun x => c * ↑x) c x

Tactic:
simpa only [mul_one] using ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal

Result:
no goals

Proof state:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x

Tactic:
rw [← mul_div_cancel_right₀ (Complex.exp (c * x)) hc]

Result:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x) * c / c) x

Proof state:
a b : ℝ
c : ℂ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c

Tactic:
have D : ∀ x : ℝ, HasDerivAt (fun y : ℝ => Complex.exp (c * y) / c) (Complex.exp (c * x)) x := by
  intro x
  conv => congr
  rw [← mul_div_cancel_right₀ (Complex.exp (c * x)) hc]
  apply ((Complex.hasDerivAt_exp _).comp x _).div_const c
  simpa only [mul_one] using ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal

Result:
a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ ∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
@[simp]
lemma CoPolarization_apply (x : N) :
    P.CoPolarization x = ∑ i, P.root' i x • P.root i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x : N
⊢ P.CoPolarization x = ∑ i : ι, (P.root' i) x • P.root i

Tactic:
simp [CoPolarization]

Result:
no goals