harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/ContinuousMap/Ordered.lean
@[simp, norm_cast]
lemma coe_sup' {ι : Type*} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)) :
    ⇑(s.sup' H f) = s.sup' H fun i ↦ ⇑(f i)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
⊢ ⇑(s.sup' H f) = s.sup' H fun i => ⇑(f i)

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x✝ : α
⊢ (s.sup' H f) x✝ = s.sup' H (fun i => ⇑(f i)) x✝

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x✝ : α
⊢ (s.sup' H f) x✝ = s.sup' H (fun i => ⇑(f i)) x✝

Tactic:
simp [sup'_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem?_modify_eq (f : α → α) (n) (l : List α) :
    (modify f n l)[n]? = f <$> l[n]?

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ (modify f n l)[n]? = f <$> l[n]?

Tactic:
simp only [getElem?_modify, if_pos]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean
theorem energy_increment (hP : P.IsEquipartition) (hP₇ : 7 ≤ #P.parts)
    (hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5) (hPα : #P.parts * 16 ^ #P.parts ≤ card α)
    (hPG : ¬P.IsUniform G ε) (hε₀ : 0 ≤ ε) (hε₁ : ε ≤ 1) :
    ↑(P.energy G) + ε ^ 5 / 4 ≤ (increment hP G ε).energy G

Proof state:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(#P.parts.offDiag) * ε ^ 5 * (22 / 75) = ↑(#P.parts.offDiag) * ε * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)

Tactic:
ring

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Nonsingular P ↔ W'.Nonsingular Q

Proof state:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Nonsingular ((fun m => m • Q) u) ↔ W'.Nonsingular Q

Tactic:
exact nonsingular_smul Q u.isUnit

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Nonsingular P ↔ W'.Nonsingular Q

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
W' : Projective R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Nonsingular ((fun m => m • Q) u) ↔ W'.Nonsingular Q
-- Mathlib/Topology/UniformSpace/HeineCantor.lean
theorem IsCompact.uniformContinuousOn_of_continuous {s : Set α} {f : α → β} (hs : IsCompact s)
    (hf : ContinuousOn f s) : UniformContinuousOn f s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : Continuous (s.restrict f)
⊢ UniformContinuous (s.restrict f)

Tactic:
exact CompactSpace.uniformContinuous_of_continuous hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuous (s.restrict f)

Tactic:
rw [isCompact_iff_compactSpace] at hs

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : ContinuousOn f s
⊢ UniformContinuous (s.restrict f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuousOn f s

Tactic:
rw [uniformContinuousOn_iff_restrict]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuous (s.restrict f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : ContinuousOn f s
⊢ UniformContinuous (s.restrict f)

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : Continuous (s.restrict f)
⊢ UniformContinuous (s.restrict f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofFin_add_rev (x : Fin (2^n)) : ofFin (x + x.rev) = allOnes n

Proof state:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
h : ↑x + (2 ^ n - (↑x + 1)) = 2 ^ n - 1
⊢ (decide (i✝ < n) && (↑x + (2 ^ n - (↑x + 1))).testBit i✝) = decide (i✝ < n)

Tactic:
rw [h, Nat.testBit_two_pow_sub_one]

Result:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
h : ↑x + (2 ^ n - (↑x + 1)) = 2 ^ n - 1
⊢ (decide (i✝ < n) && decide (i✝ < n)) = decide (i✝ < n)

Proof state:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
⊢ (↑⟨(↑x + ↑⟨2 ^ n - (↑x + 1), ⋯⟩) % 2 ^ n, ⋯⟩).testBit i✝ = decide (i✝ < n)

Tactic:
simp only [Nat.testBit_mod_two_pow, Fin.is_lt, decide_true, Bool.true_and]

Result:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
⊢ (decide (i✝ < n) && (↑x + (2 ^ n - (↑x + 1))).testBit i✝) = decide (i✝ < n)

Proof state:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
⊢ { toFin := x + x.rev }.getLsbD i✝ = (allOnes n).getLsbD i✝

Tactic:
simp only [Fin.rev, getLsbD_ofFin, getLsbD_allOnes, Fin.is_lt, decide_true]

Result:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
⊢ (↑(x + ⟨2 ^ n - (↑x + 1), ⋯⟩)).testBit i✝ = decide (i✝ < n)

Proof state:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
h : ↑x + (2 ^ n - (↑x + 1)) = 2 ^ n - 1
⊢ (decide (i✝ < n) && decide (i✝ < n)) = decide (i✝ < n)

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
x : Fin (2 ^ n)
⊢ { toFin := x + x.rev } = allOnes n

Tactic:
ext

Result:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
⊢ { toFin := x + x.rev }.getLsbD i✝ = (allOnes n).getLsbD i✝

Proof state:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
⊢ (decide (i✝ < n) && (↑x + (2 ^ n - (↑x + 1))).testBit i✝) = decide (i✝ < n)

Tactic:
have h : (x : Nat) + (2 ^ n - (x + 1)) = 2 ^ n - 1 := by omega

Result:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
h : ↑x + (2 ^ n - (↑x + 1)) = 2 ^ n - 1
⊢ (decide (i✝ < n) && (↑x + (2 ^ n - (↑x + 1))).testBit i✝) = decide (i✝ < n)

Proof state:
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
⊢ ↑x + (2 ^ n - (↑x + 1)) = 2 ^ n - 1

Tactic:
omega

Result:
no goals

Proof state:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
⊢ (↑(x + ⟨2 ^ n - (↑x + 1), ⋯⟩)).testBit i✝ = decide (i✝ < n)

Tactic:
rw [Fin.add_def]

Result:
case pred
n : Nat
x : Fin (2 ^ n)
i✝ : Nat
a✝ : i✝ < n
⊢ (↑⟨(↑x + ↑⟨2 ^ n - (↑x + 1), ⋯⟩) % 2 ^ n, ⋯⟩).testBit i✝ = decide (i✝ < n)
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_nil_right_iff {l} : Forall₂ R l nil ↔ l = nil :=
  ⟨fun H => by cases H; rfl, by rintro rfl; exact Forall₂.nil⟩

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
⊢ l = [] → Forall₂ R l []

Tactic:
rintro rfl

Result:
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Forall₂ R [] []

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
H : Forall₂ R l []
⊢ l = []

Tactic:
cases H

Result:
case nil
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ [] = []

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Forall₂ R [] []

Tactic:
exact Forall₂.nil

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ [] = []

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma hasDerivAt_Gammaℝ_one : HasDerivAt Gammaℝ (-(γ + log (4 * π)) / 2) 1

Proof state:
f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s => Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x => ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ HasDerivAt f (-log ↑π / 2 / ↑√π) 1

Tactic:
refine this.congr_deriv ?_

Result:
f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s => Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x => ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ ↑π ^ (-1 / 2) * log ↑π * (-1 / 2) = -log ↑π / 2 / ↑√π

Proof state:
f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s => Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
⊢ HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1

Tactic:
have hf : HasDerivAt f (-log π / 2 / √π) 1 := by
  have := ((hasDerivAt_neg (1 : ℂ)).div_const 2).const_cpow (c := π) (Or.inr (by norm_num))
  refine this.congr_deriv ?_
  rw [mul_assoc, ← mul_div_assoc, mul_neg_one, neg_div, cpow_neg, ← div_eq_inv_mul, aux]

Result:
f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s => Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
⊢ HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1

Proof state:
f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s => Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
⊢ -1 / 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s => Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
⊢ HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1

Tactic:
have aux2 : (√π : ℂ) ≠ 0 := by rw [ofReal_ne_zero]; positivity

Result:
f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s => Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
⊢ HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem eq_shift_mul_X_add_const (φ : R⟦X⟧) :
    φ = (mk fun p => coeff R (p + 1) φ) * X + C R (constantCoeff R φ)

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ = (mk fun p => (coeff R (p + 1)) φ) * X + (C R) ((constantCoeff R) φ)

Tactic:
ext (_ | n)

Result:
case h.zero
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff R 0) φ = (coeff R 0) ((mk fun p => (coeff R (p + 1)) φ) * X + (C R) ((constantCoeff R) φ))

case h.succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ (coeff R (n + 1)) φ = (coeff R (n + 1)) ((mk fun p => (coeff R (p + 1)) φ) * X + (C R) ((constantCoeff R) φ))

Proof state:
case h.zero
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff R 0) φ = (coeff R 0) ((mk fun p => (coeff R (p + 1)) φ) * X + (C R) ((constantCoeff R) φ))

Tactic:
simp only [coeff_zero_eq_constantCoeff, map_add, map_mul, constantCoeff_X,
  mul_zero, coeff_zero_C, zero_add]

Result:
no goals

Proof state:
case h.succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ (coeff R (n + 1)) φ = (coeff R (n + 1)) ((mk fun p => (coeff R (p + 1)) φ) * X + (C R) ((constantCoeff R) φ))

Tactic:
simp only [coeff_succ_mul_X, coeff_mk, LinearMap.map_add, coeff_C, n.succ_ne_zero, sub_zero,
  if_false, add_zero]

Result:
no goals
-- Mathlib/RingTheory/IsTensorProduct.lean
theorem IsTensorProduct.equiv_symm_apply (h : IsTensorProduct f) (x₁ : M₁) (x₂ : M₂) :
    h.equiv.symm (f x₁ x₂) = x₁ ⊗ₜ x₂

Proof state:
case a
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ h.equiv (h.equiv.symm ((f x₁) x₂)) = h.equiv (x₁ ⊗ₜ[R] x₂)

Tactic:
refine (h.equiv.apply_symm_apply _).trans ?_

Result:
case a
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ (f x₁) x₂ = h.equiv (x₁ ⊗ₜ[R] x₂)

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ h.equiv.symm ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂

Tactic:
apply h.equiv.injective

Result:
case a
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ h.equiv (h.equiv.symm ((f x₁) x₂)) = h.equiv (x₁ ⊗ₜ[R] x₂)

Proof state:
case a
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ (f x₁) x₂ = h.equiv (x₁ ⊗ₜ[R] x₂)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem pair_mem_prod {x y a b : ZFSet.{u}} : pair a b ∈ prod x y ↔ a ∈ x ∧ b ∈ y

Proof state:
x y a b : ZFSet.{u}
⊢ a.pair b ∈ x.prod y ↔ a ∈ x ∧ b ∈ y

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma add_mod_eq_ite :
    (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k

Proof state:
case neg
m n k : ℕ
h : ¬k + 1 ≤ m % (k + 1) + n % (k + 1)
⊢ (m % (k + 1) + n % (k + 1)) % (k + 1) = m % (k + 1) + n % (k + 1)

Tactic:
exact Nat.mod_eq_of_lt (Nat.lt_of_not_ge h)

Result:
no goals

Proof state:
case zero
m n : ℕ
⊢ (m + n) % 0 = if 0 ≤ m % 0 + n % 0 then m % 0 + n % 0 - 0 else m % 0 + n % 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
m n k : ℕ
⊢ (m + n) % (k + 1) =
    if k + 1 ≤ m % (k + 1) + n % (k + 1) then m % (k + 1) + n % (k + 1) - (k + 1) else m % (k + 1) + n % (k + 1)

Tactic:
rw [Nat.add_mod]

Result:
case succ
m n k : ℕ
⊢ (m % (k + 1) + n % (k + 1)) % (k + 1) =
    if k + 1 ≤ m % (k + 1) + n % (k + 1) then m % (k + 1) + n % (k + 1) - (k + 1) else m % (k + 1) + n % (k + 1)

Proof state:
case pos
m n k : ℕ
h : k + 1 ≤ m % (k + 1) + n % (k + 1)
⊢ (m % (k + 1) + n % (k + 1)) % (k + 1) =
    if k + 1 ≤ m % (k + 1) + n % (k + 1) then m % (k + 1) + n % (k + 1) - (k + 1) else m % (k + 1) + n % (k + 1)

Tactic:
rw [if_pos h, Nat.mod_eq_sub_mod h, Nat.mod_eq_of_lt]

Result:
case pos
m n k : ℕ
h : k + 1 ≤ m % (k + 1) + n % (k + 1)
⊢ m % (k + 1) + n % (k + 1) - (k + 1) < k + 1

Proof state:
case succ
m n k : ℕ
⊢ (m % (k + 1) + n % (k + 1)) % (k + 1) =
    if k + 1 ≤ m % (k + 1) + n % (k + 1) then m % (k + 1) + n % (k + 1) - (k + 1) else m % (k + 1) + n % (k + 1)

Tactic:
by_cases h : k + 1 ≤ m % (k + 1) + n % (k + 1)

Result:
case pos
m n k : ℕ
h : k + 1 ≤ m % (k + 1) + n % (k + 1)
⊢ (m % (k + 1) + n % (k + 1)) % (k + 1) =
    if k + 1 ≤ m % (k + 1) + n % (k + 1) then m % (k + 1) + n % (k + 1) - (k + 1) else m % (k + 1) + n % (k + 1)

case neg
m n k : ℕ
h : ¬k + 1 ≤ m % (k + 1) + n % (k + 1)
⊢ (m % (k + 1) + n % (k + 1)) % (k + 1) =
    if k + 1 ≤ m % (k + 1) + n % (k + 1) then m % (k + 1) + n % (k + 1) - (k + 1) else m % (k + 1) + n % (k + 1)

Proof state:
case neg
m n k : ℕ
h : ¬k + 1 ≤ m % (k + 1) + n % (k + 1)
⊢ (m % (k + 1) + n % (k + 1)) % (k + 1) =
    if k + 1 ≤ m % (k + 1) + n % (k + 1) then m % (k + 1) + n % (k + 1) - (k + 1) else m % (k + 1) + n % (k + 1)

Tactic:
rw [if_neg h]

Result:
case neg
m n k : ℕ
h : ¬k + 1 ≤ m % (k + 1) + n % (k + 1)
⊢ (m % (k + 1) + n % (k + 1)) % (k + 1) = m % (k + 1) + n % (k + 1)

Proof state:
case pos
m n k : ℕ
h : k + 1 ≤ m % (k + 1) + n % (k + 1)
⊢ m % (k + 1) + n % (k + 1) - (k + 1) < k + 1

Tactic:
exact (Nat.sub_lt_iff_lt_add h).mpr (Nat.add_lt_add (m.mod_lt (zero_lt_succ _))
  (n.mod_lt (zero_lt_succ _)))

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_le_of_forall_le {f : lp E ∞} {C : ℝ} (hC : 0 ≤ C) (hCf : ∀ i, ‖f i‖ ≤ C) :
    ‖f‖ ≤ C

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
h✝ : IsEmpty α
⊢ ‖f‖ ≤ C

case inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
h✝ : Nonempty α
⊢ ‖f‖ ≤ C

Proof state:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
h✝ : IsEmpty α
⊢ ‖f‖ ≤ C

Tactic:
simpa [eq_zero' f] using hC

Result:
no goals

Proof state:
case inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
h✝ : Nonempty α
⊢ ‖f‖ ≤ C

Tactic:
exact norm_le_of_forall_le' C hCf

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma sInf_eq_zero_iff {s : Set Cardinal} : sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0

Proof state:
case refine_2
s : Set Cardinal.{u_1}
h : s = ∅ ∨ ∃ a ∈ s, a = 0
⊢ sInf s = 0

Tactic:
rcases h with rfl | ⟨a, ha, rfl⟩

Result:
case refine_2.inl

⊢ sInf ∅ = 0

case refine_2.inr.intro.intro
s : Set Cardinal.{u_1}
ha : 0 ∈ s
⊢ sInf s = 0

Proof state:
case refine_1.inl
h : sInf ∅ = 0
⊢ ∅ = ∅ ∨ ∃ a ∈ ∅, a = 0

Tactic:
exact Or.inl rfl

Result:
no goals

Proof state:
case refine_2.inl

⊢ sInf ∅ = 0

Tactic:
exact Cardinal.sInf_empty

Result:
no goals

Proof state:
case refine_2.inr.intro.intro
s : Set Cardinal.{u_1}
ha : 0 ∈ s
⊢ sInf s = 0

Tactic:
exact eq_bot_iff.2 (csInf_le' ha)

Result:
no goals

Proof state:
s : Set Cardinal.{u_1}
⊢ sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
s : Set Cardinal.{u_1}
h : sInf s = 0
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

case refine_2
s : Set Cardinal.{u_1}
h : s = ∅ ∨ ∃ a ∈ s, a = 0
⊢ sInf s = 0

Proof state:
case refine_1.inr
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
exact Or.inr ⟨sInf s, csInf_mem hne, h⟩

Result:
no goals

Proof state:
case refine_1
s : Set Cardinal.{u_1}
h : sInf s = 0
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Result:
case refine_1.inl
h : sInf ∅ = 0
⊢ ∅ = ∅ ∨ ∃ a ∈ ∅, a = 0

case refine_1.inr
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem modPart_lt_p : modPart p r < p

Proof state:
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p = |↑p|

Tactic:
simp

Result:
no goals

Proof state:
case convert_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p ≠ 0

Tactic:
exact mod_cast hp_prime.1.ne_zero

Result:
no goals

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ modPart p r < ↑p

Tactic:
convert Int.emod_lt _ _

Result:
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p = |↑p|

case convert_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p ≠ 0
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem natDegree_of_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.toPoly.natDegree ≤ 1

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ P.toPoly.natDegree ≤ 1

Tactic:
simpa only [of_b_eq_zero ha hb] using natDegree_linear_le

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem ext_iff' {f g : α →₀ M} : f = g ↔ f.support = g.support ∧ ∀ x ∈ f.support, f x = g x :=
  ⟨fun h => h ▸ ⟨rfl, fun _ _ => rfl⟩, fun ⟨h₁, h₂⟩ =>
    ext fun a => by
      classical
      exact if h : a ∈ f.support then h₂ a h else by
        have hf : f a = 0 := not_mem_support_iff.1 h
        have hg : g a = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
⊢ f a = g a

Tactic:
exact if h : a ∈ f.support then h₂ a h else by
  have hf : f a = 0 := not_mem_support_iff.1 h
  have hg : g a = 0 := by rwa [h₁, not_mem_support_iff] at h
  rw [hf, hg]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
⊢ f a = g a

Tactic:
classical
exact if h : a ∈ f.support then h₂ a h else by
  have hf : f a = 0 := not_mem_support_iff.1 h
  have hg : g a = 0 := by rwa [h₁, not_mem_support_iff] at h
  rw [hf, hg]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
⊢ g a = 0

Tactic:
rwa [h₁, not_mem_support_iff] at h

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
⊢ f a = g a

Tactic:
have hf : f a = 0 := not_mem_support_iff.1 h

Result:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
⊢ f a = g a

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
hg : g a = 0
⊢ f a = g a

Tactic:
rw [hf, hg]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
⊢ f a = g a

Tactic:
have hg : g a = 0 := by rwa [h₁, not_mem_support_iff] at h

Result:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
hg : g a = 0
⊢ f a = g a