harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_add_aux {f g : α → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) :
    ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ :=
  calc
    ∫⁻ a, f a + g a ∂μ =
        ∫⁻ a, (⨆ n, (eapprox f n : α → ℝ≥0∞) a) + ⨆ n, (eapprox g n : α → ℝ≥0∞) a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ⨆ n, ∫⁻ (a : α), (⇑(eapprox f n) + ⇑(eapprox g n)) a ∂μ = ⨆ n, (eapprox f n).lintegral μ + (eapprox g n).lintegral μ

Tactic:
congr

Result:
case e_s
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (fun n => ∫⁻ (a : α), (⇑(eapprox f n) + ⇑(eapprox g n)) a ∂μ) = fun n =>
    (eapprox f n).lintegral μ + (eapprox g n).lintegral μ

Proof state:
case e_f.h.hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
i j : ℕ
h : i ≤ j
⊢ (fun n => (eapprox f n) a) i ≤ (fun n => (eapprox f n) a) j

Tactic:
exact monotone_eapprox _ h a

Result:
no goals

Proof state:
case e_f.h.hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Monotone fun n => (eapprox f n) a

Tactic:
intro i j h

Result:
case e_f.h.hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
i j : ℕ
h : i ≤ j
⊢ (fun n => (eapprox f n) a) i ≤ (fun n => (eapprox f n) a) j
-- Mathlib/Data/Seq/Parallel.lean
theorem parallel_empty (S : WSeq (Computation α)) (h : S.head ~> none) : parallel S = empty _ :=
  eq_empty_of_not_terminates fun ⟨⟨a, m⟩⟩ => by
    let ⟨c, cs, _⟩ := exists_of_mem_parallel m
    let ⟨n, nm⟩ := WSeq.exists_get?_of_mem cs
    let ⟨c', h'⟩ := WSeq.head_some_of_get?_some nm
    injection h h'

Proof state:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
⊢ False

Tactic:
let ⟨c, cs, _⟩ := exists_of_mem_parallel m

Result:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
⊢ False

Proof state:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
n : ℕ
nm : some c ∈ S.get? n
⊢ False

Tactic:
let ⟨c', h'⟩ := WSeq.head_some_of_get?_some nm

Result:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
n : ℕ
nm : some c ∈ S.get? n
c' : Computation α
h' : some c' ∈ S.head
⊢ False

Proof state:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
⊢ False

Tactic:
let ⟨n, nm⟩ := WSeq.exists_get?_of_mem cs

Result:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
n : ℕ
nm : some c ∈ S.get? n
⊢ False

Proof state:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
n : ℕ
nm : some c ∈ S.get? n
c' : Computation α
h' : some c' ∈ S.head
⊢ False

Tactic:
injection h h'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem eraseKey_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'}
    (h : (k' == k) = false) : eraseKey k (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: eraseKey k l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v' : β k'
h : (k' == k) = false
⊢ eraseKey k (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: eraseKey k l

Tactic:
simp [eraseKey_cons, h]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma hasEigenvalueAt (χ : Weight R L M) (x : L) :
    (toEnd R L M x).HasEigenvalue (χ x)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
⊢ ?m.173842

Tactic:
simpa [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq] using χ.genWeightSpaceOf_ne_bot x

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
⊢ ((toEnd R L M) x).HasEigenvalue (χ x)

Tactic:
obtain ⟨k : ℕ, hk : (toEnd R L M x).genEigenspace (χ x) k ≠ ⊥⟩ := by
  simpa [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq] using χ.genWeightSpaceOf_ne_bot x

Result:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
k : ℕ
hk : (((toEnd R L M) x).genEigenspace (χ x)) ↑k ≠ ⊥
⊢ ((toEnd R L M) x).HasEigenvalue (χ x)

Proof state:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
k : ℕ
hk : (((toEnd R L M) x).genEigenspace (χ x)) ↑k ≠ ⊥
⊢ ((toEnd R L M) x).HasEigenvalue (χ x)

Tactic:
exact Module.End.hasEigenvalue_of_hasGenEigenvalue hk

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertManyIfNewUnit_empty_list [EquivBEq α] [LawfulHashable α]
    {l : List α} {k : α} :
    get? (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l) k =
      if l.contains k then some () else none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
⊢ (if empty.contains k = true ∨ l.contains k = true then some () else none) =
    if l.contains k = true then some () else none

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
⊢ get? (insertManyIfNewUnit empty l).val k = if l.contains k = true then some () else none

Tactic:
rw [get?_insertManyIfNewUnit_list _ Raw.WF.empty₀]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
⊢ (if empty.contains k = true ∨ l.contains k = true then some () else none) =
    if l.contains k = true then some () else none
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem map_findSome? (f : Fin n → Option α) (g : α → β) :
    (findSome? f).map g = findSome? (Option.map g ∘ f)

Proof state:
n : Nat
α : Type u_1
β : Type u_2
f : Fin n → Option α
g : α → β
⊢ Option.map g (findSome? f) = findSome? (Option.map g ∘ f)

Tactic:
induction n with
| zero => rfl
| succ n ih => simp [findSome?_succ, Function.comp_def, Option.map_orElse, ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
β : Type u_2
g : α → β
f : Fin 0 → Option α
⊢ Option.map g (findSome? f) = findSome? (Option.map g ∘ f)

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_2
g : α → β
n : Nat
ih : ∀ (f : Fin n → Option α), Option.map g (findSome? f) = findSome? (Option.map g ∘ f)
f : Fin (n + 1) → Option α
⊢ Option.map g (findSome? f) = findSome? (Option.map g ∘ f)

Tactic:
simp [findSome?_succ, Function.comp_def, Option.map_orElse, ih]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_eq_zero_of_nonpos (h : x ≤ 0) : sqrt x = 0

Proof state:
x : ℝ
h : x ≤ 0
⊢ √x = 0

Tactic:
simp [sqrt, Real.toNNReal_eq_zero.2 h]

Result:
no goals
-- Mathlib/Algebra/Lie/TraceForm.lean
/-- A variant of `LieModule.traceForm_eq_sum_finrank_nsmul` in which the sum is taken only over the
non-zero weights. -/
lemma traceForm_eq_sum_finrank_nsmul' :
    traceForm K L M = ∑ χ ∈ {χ : Weight K L M | χ.IsNonZero}, finrank K (genWeightSpace M χ) •
      (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K)

Proof state:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
⊢ traceForm K L M =
    ∑ χ ∈ Finset.filter (fun χ => χ.IsNonZero) Finset.univ,
      finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)

Tactic:
classical
suffices ∑ χ ∈ {χ : Weight K L M | χ.IsZero}, finrank K (genWeightSpace M χ) •
    (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K) = 0 by
  rw [traceForm_eq_sum_finrank_nsmul,
    ← Finset.sum_filter_add_sum_filter_not (p := fun χ : Weight K L M ↦ χ.IsNonZero)]
  simp [this]
refine Finset.sum_eq_zero fun χ hχ ↦ ?_
replace hχ : (χ : L →ₗ[K] K) = 0 := by simpa [← Weight.coe_toLinear_eq_zero_iff] using hχ
simp [hχ]

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
χ : Weight K L M
hχ : χ ∈ Finset.filter (fun χ => χ.IsZero) Finset.univ
⊢ Weight.toLinear K L M χ = 0

Tactic:
simpa [← Weight.coe_toLinear_eq_zero_iff] using hχ

Result:
no goals
-- Mathlib/Order/Filter/Cofinite.lean
theorem le_cofinite_iff_compl_singleton_mem : l ≤ cofinite ↔ ∀ x, {x}ᶜ ∈ l

Proof state:
α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ s ∈ l

Tactic:
rw [← compl_compl s, ← biUnion_of_singleton sᶜ, compl_iUnion₂, Filter.biInter_mem hs]

Result:
α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ ∀ i ∈ sᶜ, {i}ᶜ ∈ l

Proof state:
α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ ∀ i ∈ sᶜ, {i}ᶜ ∈ l

Tactic:
exact fun x _ => h x

Result:
no goals

Proof state:
α : Type u_2
l : Filter α
⊢ l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l

Tactic:
refine ⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => ?_⟩

Result:
α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ s ∈ l
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma neg_of_Z_eq_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z = 0) :
    W.neg P = -(P y / P x) • ![1, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ Odd 3

Tactic:
decide

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ W.neg P = -(P y / P x) • ![1, 1, 0]

Tactic:
erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
  pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
  (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.neg P = -(P y / P x) • ![1, 1, 0]

Tactic:
have hX {n : ℕ} : IsUnit <| P x ^ n := (isUnit_X_of_Z_eq_zero hP hPz).pow n

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ W.neg P = -(P y / P x) • ![1, 1, 0]
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem map_mk_eq_bot_of_le {I J : Ideal R} [J.IsTwoSided] (h : I ≤ J) :
    I.map (Quotient.mk J) = ⊥

Proof state:
R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ≤ J
⊢ map (Quotient.mk J) I = ⊥

Tactic:
rw [map_eq_bot_iff_le_ker, mk_ker]

Result:
R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ≤ J
⊢ I ≤ J

Proof state:
R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ≤ J
⊢ I ≤ J

Tactic:
exact h

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
/-- The set of points `a : α` such that `κ a ⟂ₘ η a` is measurable. -/
@[measurability]
lemma measurableSet_mutuallySingular (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
    MeasurableSet {a | κ a ⟂ₘ η a}

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ MeasurableSet {a | (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0}

Tactic:
exact measurable_kernel_prod_mk_left (measurableSet_mutuallySingularSet κ η).compl
  (measurableSet_singleton 0)

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ MeasurableSet {a | κ a ⟂ₘ η a}

Tactic:
simp_rw [← withDensity_rnDeriv_eq_zero_iff_mutuallySingular,
  withDensity_rnDeriv_eq_zero_iff_measure_eq_zero]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ MeasurableSet {a | (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0}
-- Mathlib/Data/Seq/Seq.lean
theorem le_stable (s : Seq α) {m n} (h : m ≤ n) : s.get? m = none → s.get? n = none

Proof state:
α : Type u
s : Seq α
m n : ℕ
h : m ≤ n
⊢ s.get? m = none → s.get? n = none

Tactic:
obtain ⟨f, al⟩ := s

Result:
case mk
α : Type u
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : f.IsSeq
⊢ get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ n = none

Proof state:
case mk.refl
α : Type u
m n : ℕ
f : Stream' (Option α)
al : f.IsSeq
⊢ get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ m = none

case mk.step
α : Type u
m n✝ : ℕ
f : Stream' (Option α)
al : f.IsSeq
n : ℕ
a✝ : m.le n
IH : get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ n = none
⊢ get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ n.succ = none

Tactic:
exacts [id, fun h2 => al (IH h2)]

Result:
no goals

Proof state:
case mk
α : Type u
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : f.IsSeq
⊢ get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ n = none

Tactic:
induction' h with n _ IH

Result:
case mk.refl
α : Type u
m n : ℕ
f : Stream' (Option α)
al : f.IsSeq
⊢ get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ m = none

case mk.step
α : Type u
m n✝ : ℕ
f : Stream' (Option α)
al : f.IsSeq
n : ℕ
a✝ : m.le n
IH : get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ n = none
⊢ get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ n.succ = none
-- Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
theorem rank_sup_eq_rank_left_mul_rank_of_free :
    Module.rank R ↥(A ⊔ B) = Module.rank R A * Module.rank A (Algebra.adjoin A (B : Set S))

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
h✝ : Nontrivial R
a✝ : Nontrivial S
this : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)

Tactic:
letI : SMul A (Algebra.adjoin A (B : Set S)) := Algebra.toSMul

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
h✝ : Nontrivial R
a✝ : Nontrivial S
this✝ : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra
this : SMul ↥A ↥(Algebra.adjoin ↥A ↑B) := Algebra.toSMul
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)

Proof state:
case inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
h✝ : Subsingleton R
this : Subsingleton S
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
private lemma re_log_comb_nonneg {n : ℕ} (hn : 2 ≤ n) {x : ℝ} (hx : 1 < x) (y : ℝ) :
    0 ≤ 3 * (-log (1 - (1 : DirichletCharacter ℂ N) n * n ^ (-x : ℂ))).re +
          4 * (-log (1 - χ n * n ^ (-(x + I * y)))).re +
          (-log (1 - (χ n ^ 2) * n ^ (-(x + 2 * I * y)))).re

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
⊢ ↑n ^ (-x) < 1

Tactic:
rw [Real.rpow_neg (Nat.cast_nonneg n), inv_lt_one_iff₀]

Result:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
⊢ ↑n ^ x ≤ 0 ∨ 1 < ↑n ^ x

Proof state:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
⊢ 0 ≤
    3 * (-log (1 - 1 ↑n * ↑n ^ (-↑x))).re + 4 * (-log (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y)))).re +
      (-log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)))).re

Tactic:
have ha₁ : (n : ℝ) ^ (-x) < 1 := by
  rw [Real.rpow_neg (Nat.cast_nonneg n), inv_lt_one_iff₀]
  exact .inr <| Real.one_lt_rpow (mod_cast one_lt_two.trans_le hn) <| zero_lt_one.trans hx

Result:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
⊢ 0 ≤
    3 * (-log (1 - 1 ↑n * ↑n ^ (-↑x))).re + 4 * (-log (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y)))).re +
      (-log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)))).re

Proof state:
case h.e'_4.h.e'_5.h.e'_6.h.e'_6.h.e'_1.h.e'_3.e_x.e_a
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n * ↑n ^ (-(↑x + I * ↑y)) = ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y)))

Tactic:
rw [neg_add, cpow_add _ _ <| mod_cast by omega, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
  ofReal_natCast, mul_left_comm]

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
⊢ ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1

Tactic:
rw [norm_mul, ← hn'.unit_spec, DirichletCharacter.unit_norm_eq_one χ hn'.unit,
  ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (mod_cast by omega)]

Result:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
⊢ 1 * ↑n ^ (-(I * ↑y)).re = 1
-- Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
theorem exists_effectiveEpiFamily_iff_mem_induced (X : C) (S : Sieve X) :
    (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → (Y a ⟶ X)),
      EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a)) ) ↔
    (S ∈ F.inducedTopology (coherentTopology _) X)

Proof state:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (coherentTopology D)) X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
obtain ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ := (mem_sieves_iff_hasEffectiveEpiFamily _).mp hS

Result:
case refine_2.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (coherentTopology D)) X
α : Type
w✝ : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Proof state:
case refine_2.intro.intro.intro.intro.intro.refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (coherentTopology D)) X
α : Type
w✝ : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun a => ⋯.some.p
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun a => F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily (fun a => F.obj (Z a)) fun a => g₀ a ≫ π a
⊢ EffectiveEpiFamily Z fun a => F.preimage (g₀ a ≫ π a)

Tactic:
refine F.finite_effectiveEpiFamily_of_map _ _ ?_

Result:
case refine_2.intro.intro.intro.intro.intro.refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (coherentTopology D)) X
α : Type
w✝ : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun a => ⋯.some.p
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun a => F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily (fun a => F.obj (Z a)) fun a => g₀ a ≫ π a
⊢ EffectiveEpiFamily (fun a => F.obj (Z a)) fun a => F.map (F.preimage (g₀ a ≫ π a))
-- Mathlib/Data/Finmap.lean
theorem keys_erase_toFinset (a : α) (s : AList β) : keys ⟦s.erase a⟧ = (keys ⟦s⟧).erase a

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ ⟦AList.erase a s⟧.keys = ⟦s⟧.keys.erase a

Tactic:
simp [Finset.erase, keys, AList.erase, keys_kerase]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
lemma inv_def' (q : ℚ) : q⁻¹ = q.den /. q.num

Proof state:
q : ℚ
⊢ q⁻¹ = ↑q.den /. q.num

Tactic:
rw [← inv_divInt', num_divInt_den]

Result:
no goals
-- Mathlib/Data/Sum/Interval.lean
lemma Ioc_inl_inl :
    Ioc (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Ioc a₁ a₂).map (Embedding.inl.trans toLex.toEmbedding)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Ioc a₁ a₂)

Tactic:
rw [← Finset.map_map]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioc a₁ a₂))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Ioc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Ioc a₁ a₂))

Tactic:
rfl

Result:
no goals