harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- Assuming `f 0 = 0`, the `LSeries` of `f` is zero if and only if either `f = 0` or the
L-series converges nowhere. -/
lemma LSeries_eq_zero_iff {f : ℕ → ℂ} (hf : f 0 = 0) :
    LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤

Proof state:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0

Tactic:
convert (LSeries_eventually_eq_zero_iff'.mp ?_).resolve_right h

Result:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0

case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] 0

Proof state:
f : ℕ → ℂ
hf : f 0 = 0
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤

Tactic:
by_cases h : abscissaOfAbsConv f = ⊤ <;> simp [h]

Result:
case pos
f : ℕ → ℂ
hf : f 0 = 0
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0

case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0

Proof state:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f = 0

Tactic:
ext (- | m)

Result:
case a.h.zero
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f 0 = 0 0

case a.h.succ
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
m : ℕ
⊢ f (m + 1) = 0 (m + 1)

Proof state:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : f = 0
x✝¹ : ℕ
x✝ : x✝¹ ≠ 0
⊢ f x✝¹ = 0

Tactic:
rw [H', Pi.zero_apply]

Result:
no goals

Proof state:
case pos
f : ℕ → ℂ
hf : f 0 = 0
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0

Tactic:
exact LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h

Result:
no goals

Proof state:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] 0

Tactic:
simpa only [H] using Filter.EventuallyEq.rfl

Result:
no goals

Proof state:
case a.h.succ
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
m : ℕ
⊢ f (m + 1) = 0 (m + 1)

Tactic:
simp [H']

Result:
no goals

Proof state:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H ▸ LSeries_zero⟩

Result:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0

Proof state:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0

Tactic:
refine ⟨fun H' _ _ ↦ by rw [H', Pi.zero_apply], fun H' ↦ ?_⟩

Result:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f = 0

Proof state:
case a.h.zero
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f 0 = 0 0

Tactic:
simp [hf]

Result:
no goals
-- Mathlib/Algebra/Lie/LieTheorem.lean
private lemma exists_forall_lie_eq_smul_of_isSolvable_of_finite
    (L : Type*) [LieRing L] [LieAlgebra k L] [LieRingModule L V] [LieModule k L V]
    [IsSolvable L] [LieModule.IsTriangularizable k L V] [Module.Finite k L] :
    ∃ χ : Module.Dual k L, Nontrivial (weightSpace V χ)

Proof state:
case inr.intro.intro
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
lift A to LieIdeal k L

Result:
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
⊢ ∀ {x m : L}, m ∈ A → ⁅x, m⁆ ∈ A

case inr.intro.intro.intro
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
A : LieSubmodule k L L
hA : IsCoatom ↑A
hAL : ↑(derivedSeries k L 1) ≤ ↑A
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Proof state:
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
A : Submodule k L
hA : IsCoatom A
hAL : ↑(derivedSeries k L 1) ≤ A
x✝ m✝ : L
a✝ : m✝ ∈ A
⊢ ⁅x✝, m✝⁆ ∈ A

Tactic:
exact hAL <| LieSubmodule.lie_mem_lie (LieSubmodule.mem_top _) (LieSubmodule.mem_top _)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivAt.mul (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
    HasFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ HasFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x

Tactic:
convert hc.mul' hd

Result:
case h.e'_12.h.e'_6
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ d x • c' = c'.smulRight (d x)

Proof state:
case h.e'_12.h.e'_6.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
z : E
⊢ (d x • c') z = (c'.smulRight (d x)) z

Tactic:
apply mul_comm

Result:
no goals

Proof state:
case h.e'_12.h.e'_6
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ d x • c' = c'.smulRight (d x)

Tactic:
ext z

Result:
case h.e'_12.h.e'_6.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
z : E
⊢ (d x • c') z = (c'.smulRight (d x)) z
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma toAffine_of_equiv {P Q : Fin 3 → F} (h : P ≈ Q) : toAffine W P = toAffine W Q

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
h : P ≈ Q
⊢ toAffine W P = toAffine W Q

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
F : Type u
inst✝ : Field F
W : Projective F
Q : Fin 3 → F
u : Fˣ
⊢ toAffine W ((fun m => m • Q) u) = toAffine W Q

Proof state:
case intro
F : Type u
inst✝ : Field F
W : Projective F
Q : Fin 3 → F
u : Fˣ
⊢ toAffine W ((fun m => m • Q) u) = toAffine W Q

Tactic:
exact toAffine_smul Q u.isUnit

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_pair_add_mul_left {R : Type u} [CommRing R] {x y : R} (z : R) :
    (span {x + y * z, y} : Ideal R) = span {x, y}

Proof state:
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : R
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = a * (x + y * z) + b * y

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : R
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = a * x + b * y

Tactic:
ring1

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : CommRing R
x y z x✝ : R
⊢ (∃ a b, a * (x + y * z) + b * y = x✝) ↔ ∃ a b, a * x + b * y = x✝

Tactic:
exact
  ⟨fun ⟨a, b, h⟩ =>
    ⟨a, b + a * z, by
      rw [← h]
      ring1⟩,
    fun ⟨a, b, h⟩ =>
    ⟨a, b - a * z, by
      rw [← h]
      ring1⟩⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : R
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = x✝¹

Tactic:
rw [← h]

Result:
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : R
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = a * x + b * y

Proof state:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ span {x + y * z, y} = span {x, y}

Tactic:
ext

Result:
case h
R : Type u
inst✝ : CommRing R
x y z x✝ : R
⊢ x✝ ∈ span {x + y * z, y} ↔ x✝ ∈ span {x, y}

Proof state:
case h
R : Type u
inst✝ : CommRing R
x y z x✝ : R
⊢ x✝ ∈ span {x + y * z, y} ↔ x✝ ∈ span {x, y}

Tactic:
rw [mem_span_pair, mem_span_pair]

Result:
case h
R : Type u
inst✝ : CommRing R
x y z x✝ : R
⊢ (∃ a b, a * (x + y * z) + b * y = x✝) ↔ ∃ a b, a * x + b * y = x✝

Proof state:
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : R
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = x✝¹

Tactic:
rw [← h]

Result:
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : R
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = a * (x + y * z) + b * y
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_eq_one_iff (x : ℝ) : cos x = 1 ↔ ∃ n : ℤ, (n : ℝ) * (2 * π) = x :=
  ⟨fun h =>
    let ⟨n, hn⟩ := sin_eq_zero_iff.1 (sin_eq_zero_iff_cos_eq.2 (Or.inl h))
    ⟨n / 2,
      (Int.emod_two_eq_zero_or_one n).elim
        (fun hn0 => by
          rwa [← mul_assoc, ← @Int.cast_two ℝ, ← Int.cast_mul,
            Int.ediv_mul_cancel (Int.dvd_iff_emod_eq_zero.2 hn0)])
        fun hn1 => by
        rw [← Int.emod_add_ediv n 2, hn1, Int.cast_add, Int.cast_one, add_mul, one_mul, add_comm,
              mul_comm (2 : ℤ), Int.cast_mul, mul_assoc, Int.cast_two] at hn
        rw [← hn, cos_int_mul_two_pi_add_pi] at h
        exact absurd h (by norm_num)⟩,
    fun ⟨_, hn⟩ => hn ▸ cos_int_mul_two_pi _⟩

Proof state:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn0 : n % 2 = 0
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
rwa [← mul_assoc, ← @Int.cast_two ℝ, ← Int.cast_mul,
  Int.ediv_mul_cancel (Int.dvd_iff_emod_eq_zero.2 hn0)]

Result:
no goals

Proof state:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
rw [← hn, cos_int_mul_two_pi_add_pi] at h

Result:
x : ℝ
n : ℤ
h : -1 = 1
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Proof state:
x : ℝ
n : ℤ
h : -1 = 1
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
exact absurd h (by norm_num)

Result:
no goals

Proof state:
x : ℝ
n : ℤ
h : -1 = 1
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ¬-1 = 1

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑n * π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
rw [← Int.emod_add_ediv n 2, hn1, Int.cast_add, Int.cast_one, add_mul, one_mul, add_comm,
      mul_comm (2 : ℤ), Int.cast_mul, mul_assoc, Int.cast_two] at hn

Result:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem isPartition_single_iff (h : J ≤ I) : IsPartition (single I J h) ↔ J = I

Proof state:
ι : Type u_1
I J : Box ι
h : J ≤ I
⊢ (single I J h).IsPartition ↔ J = I

Tactic:
simp [isPartition_iff_iUnion_eq]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Lemmas.lean
lemma discreteTopology_of_bddAbove_range_norm {𝕜 : Type*} [NormedField 𝕜]
    (h : BddAbove (Set.range fun k : 𝕜 ↦ ‖k‖)) :
    DiscreteTopology 𝕜

Proof state:
𝕜 : Type u_4
inst✝ : NormedField 𝕜
h : BddAbove (Set.range fun k => ‖k‖)
⊢ DiscreteTopology 𝕜

Tactic:
refine (NormedField.discreteTopology_or_nontriviallyNormedField _).resolve_right ?_

Result:
𝕜 : Type u_4
inst✝ : NormedField 𝕜
h : BddAbove (Set.range fun k => ‖k‖)
⊢ ¬Nonempty { h' // NontriviallyNormedField.toNormedField = inst✝ }

Proof state:
case intro.mk.intro.intro
𝕜 : Type u_4
val✝ : NontriviallyNormedField 𝕜
x : ℝ
h : x ∈ upperBounds (Set.range fun k => ‖k‖)
k : 𝕜
hk : x < ‖k‖
⊢ False

Tactic:
exact hk.not_le (h (Set.mem_range_self k))

Result:
no goals

Proof state:
case intro.mk.intro
𝕜 : Type u_4
val✝ : NontriviallyNormedField 𝕜
x : ℝ
h : x ∈ upperBounds (Set.range fun k => ‖k‖)
⊢ False

Tactic:
obtain ⟨k, hk⟩ := NormedField.exists_lt_norm 𝕜 x

Result:
case intro.mk.intro.intro
𝕜 : Type u_4
val✝ : NontriviallyNormedField 𝕜
x : ℝ
h : x ∈ upperBounds (Set.range fun k => ‖k‖)
k : 𝕜
hk : x < ‖k‖
⊢ False

Proof state:
case intro.mk
𝕜 : Type u_4
val✝ : NontriviallyNormedField 𝕜
h : BddAbove (Set.range fun k => ‖k‖)
⊢ False

Tactic:
obtain ⟨x, h⟩ := h

Result:
case intro.mk.intro
𝕜 : Type u_4
val✝ : NontriviallyNormedField 𝕜
x : ℝ
h : x ∈ upperBounds (Set.range fun k => ‖k‖)
⊢ False

Proof state:
𝕜 : Type u_4
inst✝ : NormedField 𝕜
h : BddAbove (Set.range fun k => ‖k‖)
⊢ ¬Nonempty { h' // NontriviallyNormedField.toNormedField = inst✝ }

Tactic:
rintro ⟨_, rfl⟩

Result:
case intro.mk
𝕜 : Type u_4
val✝ : NontriviallyNormedField 𝕜
h : BddAbove (Set.range fun k => ‖k‖)
⊢ False
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
lemma card_mul_cast_addConst (A B : Finset G') : (#A * σ[A, B] : 𝕜) = #(A + B)

Proof state:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ ↑(#A) * σ[A, B] = ↑(#(A + B))

Tactic:
exact card_mul_addConst _ _

Result:
no goals

Proof state:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ ↑(#A) * ↑σ[A, B] = ↑(#(A + B))

Tactic:
norm_cast

Result:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ ↑(#A) * σ[A, B] = ↑(#(A + B))
-- Mathlib/Algebra/Polynomial/DenomsClearable.lean
theorem DenomsClearable.add {N : ℕ} {f g : R[X]} :
    DenomsClearable a b N f i → DenomsClearable a b N g i → DenomsClearable a b N (f + g) i :=
  fun ⟨Df, bf, bfu, Hf⟩ ⟨Dg, bg, bgu, Hg⟩ =>
  ⟨Df + Dg, bf, bfu, by
    rw [RingHom.map_add, Polynomial.map_add, eval_add, mul_add, Hf, Hg]
    congr
    refine @inv_unique K _ (i b) bg bf ?_ ?_ <;> rwa [mul_comm]⟩

Proof state:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bg) (Polynomial.map i g) =
    i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bf) (Polynomial.map i g)

Tactic:
congr

Result:
case e_a.e_a.e_a.e_a
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ bg = bf

Proof state:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i (Df + Dg) = i b ^ N * eval (i a * bf) (Polynomial.map i (f + g))

Tactic:
rw [RingHom.map_add, Polynomial.map_add, eval_add, mul_add, Hf, Hg]

Result:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bg) (Polynomial.map i g) =
    i b ^ N * eval (i a * bf) (Polynomial.map i f) + i b ^ N * eval (i a * bf) (Polynomial.map i g)

Proof state:
case e_a.e_a.e_a.e_a
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ bg = bf

Tactic:
refine @inv_unique K _ (i b) bg bf ?_ ?_ <;> rwa [mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
    rankD self.arr i < self.rankMax

Proof state:
self : UnionFind
i : Nat
⊢ (if h : i < self.arr.size then self.arr[i].rank else 0) < self.rankMax

Tactic:
split <;> [apply rank'_lt_rankMax; apply Nat.succ_pos]

Result:
no goals

Proof state:
self : UnionFind
i : Nat
⊢ rankD self.arr i < self.rankMax

Tactic:
simp [rankD]

Result:
self : UnionFind
i : Nat
⊢ (if h : i < self.arr.size then self.arr[i].rank else 0) < self.rankMax
-- Mathlib/Data/Finsupp/Weight.lean
lemma weight_sub_single_add {f : σ →₀ ℕ} {i : σ} (hi : f i ≠ 0) :
    (f - single i 1).weight w + w i = f.weight w

Proof state:
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ (weight w) (f - single i 1) + w i = (weight w) f

Tactic:
conv_rhs => rw [← sub_add_single_one_cancel hi, weight_apply]

Result:
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ (weight w) (f - single i 1) + w i = (f - single i 1 + single i 1).sum fun i c => c • w i

Proof state:
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ 0 • w i = 0

case h_zero
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ), 0 • w a = 0

case h_add
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ) (b₁ b₂ : ℕ), (b₁ + b₂) • w a = b₁ • w a + b₂ • w a

Tactic:
exacts [zero_smul .., fun _ ↦ zero_smul .., fun _ _ _ ↦ add_smul ..]

Result:
no goals

Proof state:
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ (weight w) (f - single i 1) + w i = (f - single i 1 + single i 1).sum fun i c => c • w i

Tactic:
rw [sum_add_index', sum_single_index, one_smul, weight_apply]

Result:
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ 0 • w i = 0

case h_zero
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ), 0 • w a = 0

case h_add
σ : Type u_1
M : Type u_2
w : σ → M
inst✝ : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : f i ≠ 0
⊢ ∀ (a : σ) (b₁ b₂ : ℕ), (b₁ + b₂) • w a = b₁ • w a + b₂ • w a
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem mutuallySingular_singularPart (μ ν : Measure α) : μ.singularPart ν ⟂ₘ ν

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ⟂ₘ ν

Tactic:
exact MutuallySingular.zero_left

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact (haveLebesgueDecomposition_spec μ ν).2.1

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
rw [singularPart_of_not_haveLebesgueDecomposition h]

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ⟂ₘ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
by_cases h : HaveLebesgueDecomposition μ ν

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ ν

case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ ν
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem card_aux₂ (hP : P.IsEquipartition) (hu : u ∈ P.parts) (hucard : #u ≠ m * 4 ^ #P.parts + a) :
    (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
⊢ m * 4 ^ #P.parts ≤ Fintype.card α / #P.parts

Tactic:
rw [stepBound, ← Nat.div_div_eq_div_mul]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
⊢ Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts ≤ Fintype.card α / #P.parts

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
⊢ Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts ≤ Fintype.card α / #P.parts

Tactic:
exact Nat.div_mul_le_self _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Tactic:
have : m * 4 ^ #P.parts ≤ card α / #P.parts := by
  rw [stepBound, ← Nat.div_div_eq_div_mul]
  exact Nat.div_mul_le_self _ _

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
this : m * 4 ^ #P.parts ≤ Fintype.card α / #P.parts
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
this : m * 4 ^ #P.parts ≤ Fintype.card α / #P.parts
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Tactic:
rw [Nat.add_sub_of_le this] at hucard

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ Fintype.card α / #P.parts
this : m * 4 ^ #P.parts ≤ Fintype.card α / #P.parts
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ Fintype.card α / #P.parts
this : m * 4 ^ #P.parts ≤ Fintype.card α / #P.parts
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Tactic:
rw [(hP.card_parts_eq_average hu).resolve_left hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
  Nat.sub_add_cancel a_add_one_le_four_pow_parts_card, ← add_assoc, mul_comm,
  Nat.add_sub_of_le this, card_univ]

Result:
no goals