harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
theorem DirichletCharacter.LSeries_eulerProduct_exp_log {N : ℕ} (χ : DirichletCharacter ℂ N)
    {s : ℂ} (hs : 1 < s.re) :
    exp (∑' p : Nat.Primes, -log (1 - χ p * p ^ (-s))) = L ↗χ s

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) = L (fun n => χ ↑n) s

Tactic:
let f := dirichletSummandHom χ <| ne_zero_of_one_lt_re hs

Result:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
⊢ cexp (∑' (p : Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) = L (fun n => χ ↑n) s

Proof state:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
n : ℕ
hn : n ≠ 0
⊢ term (fun n => χ ↑n) s n = f n

Tactic:
simp only [ne_eq, hn, not_false_eq_true, term_of_ne_zero, div_eq_mul_inv,
  dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, f]

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
h : ∀ (n : ℕ), term (fun n => χ ↑n) s n = f n
⊢ cexp (∑' (p : Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) = L (fun n => χ ↑n) s

Tactic:
simpa only [LSeries, h]
  using exp_tsum_primes_log_eq_tsum (f := f) <| summable_dirichletSummand χ hs

Result:
no goals

Proof state:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
⊢ term (fun n => χ ↑n) s 0 = f 0

Tactic:
simp only [term_zero, map_zero]

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
n : ℕ
⊢ term (fun n => χ ↑n) s n = f n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
⊢ term (fun n => χ ↑n) s 0 = f 0

case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
n : ℕ
hn : n ≠ 0
⊢ term (fun n => χ ↑n) s n = f n
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
lemma auxbound2 (c : ℝ) {d : ℝ} (hd : 1 ≤ d ^ 2) : r z ≤ ‖c * (z : ℂ) + d‖

Proof state:
z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2)
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Tactic:
simpa only [r, norm_def, normSq_apply, add_re, re_ofReal_mul, coe_re, ofReal_re, ← pow_two,
  add_im, im_ofReal_mul, coe_im, ofReal_im, add_zero, min_le_iff] using Or.inr H1

Result:
no goals

Proof state:
z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Tactic:
have H1 : √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2) :=
  (Real.sqrt_le_sqrt_iff (by positivity)).mpr (r1_aux_bound _ _ hd)

Result:
z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2)
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Proof state:
z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ 0 ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2

Tactic:
positivity

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_pos_iff' : 0 < diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y

Proof state:
β : Type u_2
inst✝ : EMetricSpace β
s : Set β
⊢ 0 < diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y

Tactic:
simp only [diam_pos_iff, Set.Nontrivial, exists_prop]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma flip_comp_polarization_eq_rootForm :
    P.flip.toLin ∘ₗ P.Polarization = P.RootForm

Proof state:
case h.h
ι : 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✝¹ x✝ : M
⊢ ((P.flip.toLin ∘ₗ P.Polarization) x✝¹) x✝ = (P.RootForm x✝¹) x✝

Tactic:
simp [rootForm_apply_apply, RootPairing.flip]

Result:
no goals

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 ι
⊢ P.flip.toLin ∘ₗ P.Polarization = P.RootForm

Tactic:
ext

Result:
case h.h
ι : 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✝¹ x✝ : M
⊢ ((P.flip.toLin ∘ₗ P.Polarization) x✝¹) x✝ = (P.RootForm x✝¹) x✝
-- Mathlib/GroupTheory/GroupAction/Defs.lean
theorem orbitRel.Quotient.mem_orbit {a : α} {x : orbitRel.Quotient G α} :
    a ∈ x.orbit ↔ Quotient.mk'' a = x

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
x : Quotient G α
⊢ a ∈ x.orbit ↔ Quotient.mk'' a = x

Tactic:
induction x using Quotient.inductionOn'

Result:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ Quotient.mk'' a = Quotient.mk'' a✝

Proof state:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ Quotient.mk'' a = Quotient.mk'' a✝

Tactic:
rw [Quotient.eq'']

Result:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ (orbitRel G α) a a✝

Proof state:
case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ (orbitRel G α) a a✝

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
@[to_additive]
lemma leftRel_prod {β : Type*} [Group β] (s' : Subgroup β) :
    leftRel (s.prod s') = (leftRel s).prod (leftRel s')

Proof state:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
⊢ leftRel (s.prod s') = (leftRel s).prod (leftRel s')

Tactic:
refine Setoid.ext fun x y ↦ ?_

Result:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (leftRel (s.prod s')) x y ↔ ((leftRel s).prod (leftRel s')) x y

Proof state:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (leftRel (s.prod s')) x y ↔ ((leftRel s).prod (leftRel s')) x y

Tactic:
rw [Setoid.prod_apply]

Result:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (leftRel (s.prod s')) x y ↔ (leftRel s) x.1 y.1 ∧ (leftRel s') x.2 y.2

Proof state:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (leftRel (s.prod s')) x y ↔ (leftRel s) x.1 y.1 ∧ (leftRel s') x.2 y.2

Tactic:
simp_rw [leftRel_apply]

Result:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ x⁻¹ * y ∈ s.prod s' ↔ x.1⁻¹ * y.1 ∈ s ∧ x.2⁻¹ * y.2 ∈ s'

Proof state:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ x⁻¹ * y ∈ s.prod s' ↔ x.1⁻¹ * y.1 ∈ s ∧ x.2⁻¹ * y.2 ∈ s'

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_sub_self_right {m n : ℕ} (h : m ≤ n) : gcd m (n - m) = gcd m n

Proof state:
m n : ℕ
h : m ≤ n
⊢ m.gcd (n - m) = m.gcd n

Tactic:
rw [gcd_comm, gcd_sub_self_left h, gcd_comm]

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
lemma bodd_eq_one_and_ne_zero : ∀ n, bodd n = (1 &&& n != 0)
  | 0 => rfl
  | 1 => rfl
  | n + 2 => by simpa using bodd_eq_one_and_ne_zero n

Proof state:
n : ℕ
⊢ (n + 2).bodd = (1 &&& n + 2 != 0)

Tactic:
simpa using bodd_eq_one_and_ne_zero n

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_neg (a b : α) : toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)

Tactic:
rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem erase_empty {k : α} {c : Nat} : (empty c : Raw α β).erase k = empty c

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
c : Nat
⊢ (empty c).WF

Tactic:
wf_trivial

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
c : Nat
⊢ (empty c).erase k = empty c

Tactic:
rw [erase_eq (by wf_trivial)]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
c : Nat
⊢ (Raw₀.erase ⟨empty c, ⋯⟩ k).val = empty c

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
c : Nat
⊢ (Raw₀.erase ⟨empty c, ⋯⟩ k).val = empty c

Tactic:
exact congrArg Subtype.val Raw₀.erase_empty

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.dual : ∀ {t : Ordnode α} {o₁ o₂}, Valid' o₁ t o₂ → @Valid' αᵒᵈ _ o₂ (dual t) o₁
  | .nil, _, _, h => valid'_nil h.1.dual
  | .node _ l _ r, _, _, ⟨⟨ol, Or⟩, ⟨rfl, sl, sr⟩, ⟨b, bl, br⟩⟩ =>
    let ⟨ol', sl', bl'⟩ := Valid'.dual ⟨ol, sl, bl⟩
    let ⟨or', sr', br'⟩ := Valid'.dual ⟨Or, sr, br⟩
    ⟨⟨or', ol'⟩, ⟨by simp [size_dual, add_comm], sr', sl'⟩,
      ⟨by rw [size_dual, size_dual]; exact b.symm, br', bl'⟩⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ l.size + r.size + 1 = r.dual.size + l.dual.size + 1

Tactic:
simp [size_dual, add_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.size l.size

Tactic:
exact b.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.dual.size l.dual.size

Tactic:
rw [size_dual, size_dual]

Result:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.size l.size
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toENNRealVectorMeasure_add (μ ν : Measure α) :
    (μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ (μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure

Tactic:
refine MeasureTheory.VectorMeasure.ext fun i hi => ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ ↑(μ + ν).toENNRealVectorMeasure i = ↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) i

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ ↑(μ + ν).toENNRealVectorMeasure i = ↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) i

Tactic:
rw [toENNRealVectorMeasure_apply_measurable hi, add_apply, VectorMeasure.add_apply,
  toENNRealVectorMeasure_apply_measurable hi, toENNRealVectorMeasure_apply_measurable hi]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mul_add_inv_left {g : R →+* P} (h : ∀ y : M, IsUnit (g y)) (y : M) (w z₁ z₂ : P) :
    w * ↑(IsUnit.liftRight (g.toMonoidHom.restrict M) h y)⁻¹ + z₁ =
    z₂ ↔ w + g y * z₁ = g y * z₂

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ w + ((↑g).restrict M) y * z₁ = ((↑g).restrict M) y * z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂

Tactic:
simp [RingHom.toMonoidHom_eq_coe, MonoidHom.restrict_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ w * ↑((IsUnit.liftRight ((↑g).restrict M) h) y)⁻¹ + z₁ = z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂

Tactic:
rw [mul_comm, ← one_mul z₁, ← Units.inv_mul (IsUnit.liftRight (g.toMonoidHom.restrict M) h y),
  mul_assoc, ← mul_add, Units.inv_mul_eq_iff_eq_mul, Units.inv_mul_cancel_left,
  IsUnit.coe_liftRight]

Result:
R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ w + ((↑g).restrict M) y * z₁ = ((↑g).restrict M) y * z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂
-- Mathlib/Analysis/Meromorphic/Basic.lean
@[fun_prop]
lemma pow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℕ) : MeromorphicAt (f ^ n) x

Proof state:
case zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
⊢ MeromorphicAt (f ^ 0) x

Tactic:
simpa only [pow_zero] using MeromorphicAt.const 1 x

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
⊢ MeromorphicAt (f ^ n) x

Tactic:
induction n with
| zero => simpa only [pow_zero] using MeromorphicAt.const 1 x
| succ m hm => simpa only [pow_succ] using hm.mul hf

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm : MeromorphicAt (f ^ m) x
⊢ MeromorphicAt (f ^ (m + 1)) x

Tactic:
simpa only [pow_succ] using hm.mul hf

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_nat_eq_addSubmonoid_closure (s : Set M) :
    (span ℕ s).toAddSubmonoid = AddSubmonoid.closure s

Proof state:
M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ span ℕ s ≤ AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s)

Tactic:
rw [span_le]

Result:
M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ s ⊆ ↑(AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s))

Proof state:
M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ s ⊆ ↑(AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s))

Tactic:
exact AddSubmonoid.subset_closure

Result:
no goals

Proof state:
M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ (span ℕ s).toAddSubmonoid = AddSubmonoid.closure s

Tactic:
refine Eq.symm (AddSubmonoid.closure_eq_of_le subset_span ?_)

Result:
M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ (span ℕ s).toAddSubmonoid ≤ AddSubmonoid.closure s

Proof state:
M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ (span ℕ s).toAddSubmonoid ≤ AddSubmonoid.closure s

Tactic:
apply (OrderIso.to_galoisConnection (AddSubmonoid.toNatSubmodule (M := M)).symm).l_le
   (a := span ℕ s) (b := AddSubmonoid.closure s)

Result:
M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ span ℕ s ≤ AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s)
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
theorem epi_of_mono_of_epi_of_mono (hR₁ : R₁.Exact)
    (hR₂' : Mono R₂.f) (h₀ : Epi φ.τ₂) (h₁ : Mono φ.τ₃) : Epi φ.τ₁ :=
  Abelian.epi_of_mono_of_epi_of_mono' (ShortComplex.mapToComposableArrows φ)
    hR₁.exact_toComposableArrows (by simp) hR₂' h₀ h₁

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ShortComplex C
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono R₂.f
h₀ : Epi φ.τ₂
h₁ : Mono φ.τ₃
⊢ R₂.toComposableArrows.map' 0 2 ⋯ ⋯ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem connectedComponentIn_eq {x y : α} {F : Set α} (h : y ∈ connectedComponentIn F x) :
    connectedComponentIn F x = connectedComponentIn F y

Proof state:
case intro.mk.intro
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
y : α
hy : y ∈ F
h2y : ⟨y, hy⟩ ∈ connectedComponent ⟨x, hx⟩
⊢ Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponentIn F ↑⟨y, hy⟩

Tactic:
simp_rw [connectedComponentIn_eq_image hy, connectedComponent_eq h2y]

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
hx : x ∈ F
⊢ connectedComponentIn F x = connectedComponentIn F y

Tactic:
simp_rw [connectedComponentIn_eq_image hx] at h ⊢

Result:
α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
hx : x ∈ F
h : y ∈ Subtype.val '' connectedComponent ⟨x, hx⟩
⊢ Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponentIn F y

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
hx : x ∈ F
h : y ∈ Subtype.val '' connectedComponent ⟨x, hx⟩
⊢ Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponentIn F y

Tactic:
obtain ⟨⟨y, hy⟩, h2y, rfl⟩ := h

Result:
case intro.mk.intro
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
y : α
hy : y ∈ F
h2y : ⟨y, hy⟩ ∈ connectedComponent ⟨x, hx⟩
⊢ Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponentIn F ↑⟨y, hy⟩

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x = connectedComponentIn F y

Tactic:
have hx : x ∈ F := connectedComponentIn_nonempty_iff.mp ⟨y, h⟩

Result:
α : Type u
inst✝ : TopologicalSpace α
x y : α
F : Set α
h : y ∈ connectedComponentIn F x
hx : x ∈ F
⊢ connectedComponentIn F x = connectedComponentIn F y
-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_le_of_forall_moveLeft {G : PGame} {o : Nimber}
    (h : ∀ i, grundyValue (G.moveLeft i) ≠ o) : G.grundyValue ≤ o

Proof state:
G : PGame
o : Nimber
h : ∀ (i : G.LeftMoves), (G.moveLeft i).grundyValue ≠ o
⊢ G.grundyValue ≤ o

Tactic:
contrapose! h

Result:
G : PGame
o : Nimber
h : o < G.grundyValue
⊢ ∃ i, (G.moveLeft i).grundyValue = o

Proof state:
G : PGame
o : Nimber
h : o < G.grundyValue
⊢ ∃ i, (G.moveLeft i).grundyValue = o

Tactic:
exact exists_grundyValue_moveLeft_of_lt h

Result:
no goals
-- Mathlib/Probability/Kernel/CondDistrib.lean
/-- If the singleton `{x}` has non-zero mass for `μ.map X`, then for all `s : Set Ω`,
`condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s)` . -/
lemma condDistrib_apply_of_ne_zero [MeasurableSingletonClass β]
    (hY : Measurable Y) (x : β) (hX : μ.map X {x} ≠ 0) (s : Set Ω) :
    condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ (Measure.map (fun a => (X a, Y a)) μ).fst {x} ≠ 0

Tactic:
rwa [Measure.fst_map_prod_mk hY]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ ((condDistrib Y X μ) x) s = ((Measure.map X μ) {x})⁻¹ * (Measure.map (fun a => (X a, Y a)) μ) ({x} ×ˢ s)

Tactic:
rw [condDistrib, Measure.condKernel_apply_of_ne_zero _ s]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ ((Measure.map (fun a => (X a, Y a)) μ).fst {x})⁻¹ * (Measure.map (fun a => (X a, Y a)) μ) ({x} ×ˢ s) =
    ((Measure.map X μ) {x})⁻¹ * (Measure.map (fun a => (X a, Y a)) μ) ({x} ×ˢ s)

α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ (Measure.map (fun a => (X a, Y a)) μ).fst {x} ≠ 0

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : (Measure.map X μ) {x} ≠ 0
s : Set Ω
⊢ ((Measure.map (fun a => (X a, Y a)) μ).fst {x})⁻¹ * (Measure.map (fun a => (X a, Y a)) μ) ({x} ×ˢ s) =
    ((Measure.map X μ) {x})⁻¹ * (Measure.map (fun a => (X a, Y a)) μ) ({x} ×ˢ s)

Tactic:
rw [Measure.fst_map_prod_mk hY]

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
theorem map_polynomial_aeval_of_nonempty [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X])
    (hnon : (σ a).Nonempty) : σ (aeval a p) = (fun k => eval k p) '' σ a

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
⊢ σ ((aeval a) p) = (fun k => eval k p) '' σ a

Tactic:
nontriviality A

Result:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
⊢ σ ((aeval a) p) = (fun k => eval k p) '' σ a

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
⊢ σ ((aeval a) p) = (fun k => eval k p) '' σ a

Tactic:
refine Or.elim (le_or_gt (degree p) 0) (fun h => ?_) (map_polynomial_aeval_of_degree_pos a p)

Result:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
h : p.degree ≤ 0
⊢ σ ((aeval a) p) = (fun k => eval k p) '' σ a

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
h : p.degree ≤ 0
⊢ σ ((aeval a) (C (p.coeff 0))) = (fun k => eval k (C (p.coeff 0))) '' σ a

Tactic:
simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]

Result:
no goals

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
h : p.degree ≤ 0
⊢ σ ((aeval a) p) = (fun k => eval k p) '' σ a

Tactic:
rw [eq_C_of_degree_le_zero h]

Result:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
h : p.degree ≤ 0
⊢ σ ((aeval a) (C (p.coeff 0))) = (fun k => eval k (C (p.coeff 0))) '' σ a