harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_eq_one_iff {w : W} : ℓ w = 1 ↔ ∃ i : B, w = s i

Proof state:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ (∃ i, w = cs.simple i) → cs.length w = 1

Tactic:
rintro ⟨i, rfl⟩

Result:
case mpr.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.length (cs.simple i) = 1

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w = 1 ↔ ∃ i, w = cs.simple i

Tactic:
constructor

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w = 1 → ∃ i, w = cs.simple i

case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ (∃ i, w = cs.simple i) → cs.length w = 1

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w = 1 → ∃ i, w = cs.simple i

Tactic:
intro h

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
h : cs.length w = 1
⊢ ∃ i, w = cs.simple i

Proof state:
case mpr.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.length (cs.simple i) = 1

Tactic:
exact cs.length_simple i

Result:
no goals

Proof state:
case mp.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.length (cs.wordProd ω) = 1
hω : ω.length = cs.length (cs.wordProd ω)
⊢ ∃ i, cs.wordProd ω = cs.simple i

Tactic:
rcases List.length_eq_one.mp (hω.trans h) with ⟨i, rfl⟩

Result:
case mp.intro.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
h : cs.length (cs.wordProd [i]) = 1
hω : [i].length = cs.length (cs.wordProd [i])
⊢ ∃ i_1, cs.wordProd [i] = cs.simple i_1

Proof state:
case mp.intro.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
h : cs.length (cs.wordProd [i]) = 1
hω : [i].length = cs.length (cs.wordProd [i])
⊢ ∃ i_1, cs.wordProd [i] = cs.simple i_1

Tactic:
exact ⟨i, cs.wordProd_singleton i⟩

Result:
no goals

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
h : cs.length w = 1
⊢ ∃ i, w = cs.simple i

Tactic:
rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩

Result:
case mp.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.length (cs.wordProd ω) = 1
hω : ω.length = cs.length (cs.wordProd ω)
⊢ ∃ i, cs.wordProd ω = cs.simple i
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_multiset_of_countable (α : Type u) [Countable α] [Nonempty α] : #(Multiset α) = ℵ₀

Proof state:
α : Type u
inst✝¹ : Countable α
inst✝ : Nonempty α
⊢ #(Multiset α) = ℵ₀

Tactic:
classical
exact Multiset.toFinsupp.toEquiv.cardinal_eq.trans (by simp)

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Countable α
inst✝ : Nonempty α
⊢ #(α →₀ ℕ) = ℵ₀

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Countable α
inst✝ : Nonempty α
⊢ #(Multiset α) = ℵ₀

Tactic:
exact Multiset.toFinsupp.toEquiv.cardinal_eq.trans (by simp)

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xz_succ_succ (n) : xz a1 (n + 2) = (2 * a : ℕ) * xz a1 (n + 1) - xz a1 n :=
  eq_sub_of_add_eq <| by delta xz; rw [← Int.ofNat_add, ← Int.ofNat_mul, xn_succ_succ]

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(xn a1 (n + 2)) + ↑(xn a1 n) = ↑(2 * a) * ↑(xn a1 (n + 1))

Tactic:
rw [← Int.ofNat_add, ← Int.ofNat_mul, xn_succ_succ]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ xz a1 (n + 2) + xz a1 n = ↑(2 * a) * xz a1 (n + 1)

Tactic:
delta xz

Result:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(xn a1 (n + 2)) + ↑(xn a1 n) = ↑(2 * a) * ↑(xn a1 (n + 1))
-- Mathlib/Data/PNat/Xgcd.lean
theorem flip_isSpecial : (flip u).IsSpecial ↔ u.IsSpecial

Proof state:
u : XgcdType
⊢ u.flip.IsSpecial ↔ u.IsSpecial

Tactic:
dsimp [IsSpecial, flip]

Result:
u : XgcdType
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y

Proof state:
u : XgcdType
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y

Tactic:
rw [mul_comm u.x, mul_comm u.zp, add_comm u.zp]

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
lemma isAtom_iff : IsAtom s ↔ ∃ a, s = {a}

Proof state:
α : Type u_1
s : Multiset α
⊢ IsAtom s ↔ ∃ a, s = {a}

Tactic:
simp [← bot_covBy_iff, covBy_iff, eq_comm]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem max_def_lt (x y : α) : max x y = if x < y then y else x

Proof state:
α : Type u_2
inst✝ : LinearOrder α
x y : α
⊢ x ⊔ y = if x < y then y else x

Tactic:
rw [max_comm, max_def, ← ite_not]

Result:
α : Type u_2
inst✝ : LinearOrder α
x y : α
⊢ (if ¬y ≤ x then y else x) = if x < y then y else x

Proof state:
α : Type u_2
inst✝ : LinearOrder α
x y : α
⊢ (if ¬y ≤ x then y else x) = if x < y then y else x

Tactic:
simp only [not_le]

Result:
no goals
-- Mathlib/RingTheory/Localization/Finiteness.lean
/-- If `I` is an ideal such that there exists a set `{ r }` of `R` such
that the image of `I` in `Rᵣ` is finitely generated for each `r`, then `I` is finitely
generated. -/
lemma fg_of_localizationSpan {I : Ideal R} (t : Set R) (ht : Ideal.span t = ⊤)
    (H : ∀ (g : t), (I.map (algebraMap R (Localization.Away g.val))).FG) : I.FG

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
t : Set R
ht : span t = ⊤
H : ∀ (g : ↑t), (map (algebraMap R (Localization.Away ↑g)) I).FG
k : (g : ↑t) → ↥I →ₗ[R] ↥(map (algebraMap R (Localization.Away ↑g)) I) :=
  fun g => Algebra.idealMap (Localization.Away ↑g) I
⊢ Module.Finite R ↥I

Tactic:
exact Module.Finite.of_localizationSpan' t ht k (fun g ↦ Module.Finite.iff_fg.mpr (H g))

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
t : Set R
ht : span t = ⊤
H : ∀ (g : ↑t), (map (algebraMap R (Localization.Away ↑g)) I).FG
⊢ Module.Finite R ↥I

Tactic:
let k (g : t) : I →ₗ[R] (I.map (algebraMap R (Localization.Away g.val))) :=
  Algebra.idealMap I (S := Localization.Away g.val)

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
t : Set R
ht : span t = ⊤
H : ∀ (g : ↑t), (map (algebraMap R (Localization.Away ↑g)) I).FG
k : (g : ↑t) → ↥I →ₗ[R] ↥(map (algebraMap R (Localization.Away ↑g)) I) :=
  fun g => Algebra.idealMap (Localization.Away ↑g) I
⊢ Module.Finite R ↥I

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
t : Set R
ht : span t = ⊤
H : ∀ (g : ↑t), (map (algebraMap R (Localization.Away ↑g)) I).FG
⊢ I.FG

Tactic:
apply Module.Finite.iff_fg.mp

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
t : Set R
ht : span t = ⊤
H : ∀ (g : ↑t), (map (algebraMap R (Localization.Away ↑g)) I).FG
⊢ Module.Finite R ↥I
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem arithShiftRightNat_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') :
    BitVec.sshiftRight x' n = BitVec.sshiftRight x n

Proof state:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x'.sshiftRight n = x.sshiftRight n

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Order/Monotone/Defs.lean
lemma monotone_iff_apply₂ : Monotone f ↔ ∀ i, Monotone (f · i)

Proof state:
ι : Type u_1
α : Type u
β : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (β i)
inst✝ : Preorder α
f : α → (i : ι) → β i
⊢ Monotone f ↔ ∀ (i : ι), Monotone fun x => f x i

Tactic:
simp [Monotone, Pi.le_def, @forall_swap ι]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn_cons [Monad m] (f : α → β → m (ForInStep β)) (a : α) (as : List α) (b : β) :
    forIn (a::as) b f = f a b >>= fun | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m (ForInStep β)
a : α
as : List α
b : β
this :
  (forIn' (a :: as) b fun a' x b => f a' b) = do
    let x ← f a b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' as b fun a' m b => f a' b
⊢ forIn (a :: as) b f = do
    let x ← f a b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn as b f

Tactic:
simpa only [forIn'_eq_forIn]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m (ForInStep β)
a : α
as : List α
b : β
⊢ forIn (a :: as) b f = do
    let x ← f a b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn as b f

Tactic:
have := forIn'_cons (a := a) (as := as) (fun a' _ b => f a' b) b

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m (ForInStep β)
a : α
as : List α
b : β
this :
  (forIn' (a :: as) b fun a' x b => f a' b) = do
    let x ← f a b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' as b fun a' m b => f a' b
⊢ forIn (a :: as) b f = do
    let x ← f a b
    match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn as b f
-- Mathlib/Data/Nat/Squarefree.lean
theorem sq_mul_squarefree (n : ℕ) : ∃ a b : ℕ, b ^ 2 * a = n ∧ Squarefree a

Proof state:
case zero

⊢ ∃ a b, b ^ 2 * a = 0 ∧ Squarefree a

Tactic:
exact ⟨1, 0, by simp, squarefree_one⟩

Result:
no goals

Proof state:
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n ∧ Squarefree a

Tactic:
rcases n with - | n

Result:
case zero

⊢ ∃ a b, b ^ 2 * a = 0 ∧ Squarefree a

case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a

Proof state:
case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a

Tactic:
obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n)

Result:
case succ.intro.intro.intro.intro.intro
n a b : ℕ
h₁ : b ^ 2 * a = n.succ
h₂ : Squarefree a
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a

Proof state:
⊢ 0 ^ 2 * 1 = 0

Tactic:
simp

Result:
no goals

Proof state:
case succ.intro.intro.intro.intro.intro
n a b : ℕ
h₁ : b ^ 2 * a = n.succ
h₂ : Squarefree a
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a

Tactic:
exact ⟨a, b, h₁, h₂⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_union_le (f : α → ℝ≥0∞) (s t : Set α) :
    ∫⁻ a in s ∪ t, f a ∂μ ≤ ∫⁻ a in s, f a ∂μ + ∫⁻ a in t, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
⊢ ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in t, f a ∂μ

Tactic:
rw [← lintegral_add_measure]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
⊢ ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α), f a ∂(μ.restrict s + μ.restrict t)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
⊢ ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α), f a ∂(μ.restrict s + μ.restrict t)

Tactic:
exact lintegral_mono' (restrict_union_le _ _) le_rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem nat_power_eq {c : Cardinal.{u}} (h : ℵ₀ ≤ c) {n : ℕ} (hn : 2 ≤ n) :
    (n : Cardinal.{u}) ^ c = 2 ^ c :=
  power_eq_two_power h (by assumption_mod_cast) ((nat_lt_aleph0 n).le.trans h)

Proof state:
c : Cardinal.{u}
h : ℵ₀ ≤ c
n : ℕ
hn : 2 ≤ n
⊢ 2 ≤ ↑n

Tactic:
assumption_mod_cast

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem updateRow_conjTranspose [DecidableEq n] [Star α] :
    updateRow Mᴴ j (star c) = (updateCol M j c)ᴴ

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ Mᴴ.updateRow j (star c) = (M.updateCol j c)ᴴ

Tactic:
rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateRow_transpose,
  map_updateCol]

Result:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ ((M.map star).updateCol j (star c))ᵀ = ((M.map star).updateCol j (star ∘ c))ᵀ

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ ((M.map star).updateCol j (star c))ᵀ = ((M.map star).updateCol j (star ∘ c))ᵀ

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_indicator_const (hT : DominatedFinMeasAdditive μ T C) {s : Set α}
    (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E) :
    setToFun μ T hT (s.indicator fun _ => x) = T s x

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
⊢ setToFun μ T hT ↑↑(indicatorConstLp 1 hs hμs x) = (T s) x

Tactic:
rw [L1.setToFun_eq_setToL1 hT]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
⊢ (L1.setToL1 hT) (indicatorConstLp 1 hs hμs x) = (T s) x

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
⊢ (L1.setToL1 hT) (indicatorConstLp 1 hs hμs x) = (T s) x

Tactic:
exact L1.setToL1_indicatorConstLp hT hs hμs x

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
⊢ setToFun μ T hT (s.indicator fun x_1 => x) = (T s) x

Tactic:
rw [setToFun_congr_ae hT (@indicatorConstLp_coeFn _ _ _ 1 _ _ _ hs hμs x).symm]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
⊢ setToFun μ T hT ↑↑(indicatorConstLp 1 hs hμs x) = (T s) x
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem min_le_padicValRat_add {q r : ℚ} (hqr : q + r ≠ 0) :
    min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r) :=
  (le_total (padicValRat p q) (padicValRat p r)).elim
  (fun h => by rw [min_eq_left h]; exact le_padicValRat_add_of_le hqr h)
  (fun h => by rw [min_eq_right h, add_comm]; exact le_padicValRat_add_of_le (by rwa [add_comm]) h)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ r + q ≠ 0

Tactic:
rwa [add_comm]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ padicValRat p r ≤ padicValRat p (r + q)

Tactic:
exact le_padicValRat_add_of_le (by rwa [add_comm]) h

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)

Tactic:
rw [min_eq_right h, add_comm]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ padicValRat p r ≤ padicValRat p (r + q)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
⊢ padicValRat p q ⊓ padicValRat p r ≤ padicValRat p (q + r)

Tactic:
rw [min_eq_left h]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
⊢ padicValRat p q ≤ padicValRat p (q + r)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
exact le_padicValRat_add_of_le hqr h

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem mem_nhds_subtype_iff_nhdsWithin {s : Set α} {a : s} {t : Set s} :
    t ∈ 𝓝 a ↔ (↑) '' t ∈ 𝓝[s] (a : α)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : ↑s
t : Set ↑s
⊢ t ∈ 𝓝 a ↔ Subtype.val '' t ∈ 𝓝[s] ↑a

Tactic:
rw [← map_nhds_subtype_val, image_mem_map_iff Subtype.val_injective]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
/-- The function `fun x ↦ f x / r` tends to negative infinity along a nontrivial filter
if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity. -/
lemma tendsto_div_const_atBot_iff [NeBot l] :
    Tendsto (fun x ↦ f x / r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x => f x / r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem preimage_image_mk_closed (hs : IsClosed s) : mk ⁻¹' (mk '' s) = s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ mk ⁻¹' (mk '' s) ⊆ s

Tactic:
rintro x ⟨y, hys, hxy⟩

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
x y : X
hys : y ∈ s
hxy : mk y = mk x
⊢ x ∈ s

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
x y : X
hys : y ∈ s
hxy : mk y = mk x
⊢ x ∈ s

Tactic:
exact ((mk_eq_mk.1 hxy).mem_closed_iff hs).1 hys

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ mk ⁻¹' (mk '' s) = s

Tactic:
refine Subset.antisymm ?_ (subset_preimage_image _ _)

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ mk ⁻¹' (mk '' s) ⊆ s
-- Mathlib/Order/Filter/Basic.lean
theorem eventuallyEq_iff_sub [AddGroup β] {f g : α → β} {l : Filter α} :
    f =ᶠ[l] g ↔ f - g =ᶠ[l] 0 :=
  ⟨fun h => h.sub_eq, fun h => by simpa using h.add (EventuallyEq.refl l g)⟩

Proof state:
α : Type u
β : Type v
inst✝ : AddGroup β
f g : α → β
l : Filter α
h : f - g =ᶠ[l] 0
⊢ f =ᶠ[l] g

Tactic:
simpa using h.add (EventuallyEq.refl l g)

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem continuousWithinAt_iff'_right [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
    ContinuousWithinAt f s b ↔ Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)

Tactic:
rw [ContinuousWithinAt, tendsto_nhds_right]

Result:
no goals
-- Mathlib/Data/Finsupp/Weight.lean
theorem le_weight_of_ne_zero (hw : ∀ s, 0 ≤ w s) {s : σ} {f : σ →₀ ℕ} (hs : f s ≠ 0) :
    w s ≤ weight w f

Proof state:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ 1 ≤ f s

Tactic:
exact Nat.one_le_iff_ne_zero.mpr hs

Result:
no goals

Proof state:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : s ∈ f.support
⊢ f s • w s ≤ f s • w s + ∑ x ∈ f.support \ {s}, f x • w x

Tactic:
exact le_add_of_nonneg_right <| Finset.sum_nonneg <|
  fun i _ ↦ nsmul_nonneg (hw i) (f i)

Result:
no goals

Proof state:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ f s • w s

Tactic:
apply le_smul_of_one_le_left (hw s)

Result:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ 1 ≤ f s

Proof state:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ f s • w s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
rw [← Finsupp.mem_support_iff] at hs

Result:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : s ∈ f.support
⊢ f s • w s ≤ ∑ x ∈ f.support, f x • w x

Proof state:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ (weight w) f

Tactic:
simp only [weight_apply, Finsupp.sum]

Result:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ ∑ x ∈ f.support, f x • w x

Proof state:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : s ∈ f.support
⊢ f s • w s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton hs]

Result:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : s ∈ f.support
⊢ f s • w s ≤ f s • w s + ∑ x ∈ f.support \ {s}, f x • w x

Proof state:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
trans f s • w s

Result:
σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ f s • w s

σ : Type u_1
M : Type u_2
inst✝ : OrderedAddCommMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ f s • w s ≤ ∑ x ∈ f.support, f x • w x
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem rankD_set {arr : Array UFNode} {x v i h} :
    rankD (arr.set x v h) i = if x = i then v.rank else rankD arr i

Proof state:
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
⊢ (if h_1 : i < arr.size then (arr.set x v h)[i].rank else 0) =
    if x = i then v.rank else if h : i < arr.size then arr[i].rank else 0

Tactic:
split

Result:
case isTrue
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
h✝ : i < arr.size
⊢ (arr.set x v h)[i].rank = if x = i then v.rank else arr[i].rank

case isFalse
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
h✝ : ¬i < arr.size
⊢ 0 = if x = i then v.rank else 0

Proof state:
case isFalse.isTrue
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
h✝¹ : ¬i < arr.size
h✝ : x = i
⊢ 0 = v.rank

Tactic:
subst i

Result:
case isFalse.isTrue
arr : Array UFNode
x : Nat
v : UFNode
h : x < arr.size
h✝ : ¬x < arr.size
⊢ 0 = v.rank

Proof state:
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
⊢ rankD (arr.set x v h) i = if x = i then v.rank else rankD arr i

Tactic:
rw [rankD]

Result:
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
⊢ (if h_1 : i < (arr.set x v h).size then (arr.set x v h)[i].rank else 0) = if x = i then v.rank else rankD arr i

Proof state:
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
⊢ (if h_1 : i < (arr.set x v h).size then (arr.set x v h)[i].rank else 0) = if x = i then v.rank else rankD arr i

Tactic:
simp only [Array.size_set, Array.get_eq_getElem, rankD]

Result:
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
⊢ (if h_1 : i < arr.size then (arr.set x v h)[i].rank else 0) =
    if x = i then v.rank else if h : i < arr.size then arr[i].rank else 0

Proof state:
case isFalse.isTrue
arr : Array UFNode
x : Nat
v : UFNode
h : x < arr.size
h✝ : ¬x < arr.size
⊢ 0 = v.rank

Tactic:
cases ‹¬_› h

Result:
no goals

Proof state:
case isFalse
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
h✝ : ¬i < arr.size
⊢ 0 = if x = i then v.rank else 0

Tactic:
split <;> [(subst i; cases ‹¬_› h); rfl]

Result:
no goals

Proof state:
case isTrue
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
h✝ : i < arr.size
⊢ (arr.set x v h)[i].rank = if x = i then v.rank else arr[i].rank

Tactic:
split <;> simp_all

Result:
no goals