harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {x : α} {i : Nat} {l : Vector α n} {k : Nat} :
    (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = x

Proof state:
case mk
α : Type u_1
x : α
i k : Nat
l : Array α
⊢ (x, i) ∈ { toArray := l, size_toArray := ⋯ }.zipIdx k ↔ k ≤ i ∧ { toArray := l, size_toArray := ⋯ }[i - k]? = some x

Tactic:
simp [Array.mk_mem_zipIdx_iff_le_and_getElem?_sub]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
x : α
i : Nat
l : Vector α n
k : Nat
⊢ (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = some x

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
x : α
i k : Nat
l : Array α
⊢ (x, i) ∈ { toArray := l, size_toArray := ⋯ }.zipIdx k ↔ k ≤ i ∧ { toArray := l, size_toArray := ⋯ }[i - k]? = some x
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_eq_coe_fintype_card [Fintype α] : card α = Fintype.card α

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ card α = ↑(Fintype.card α)

Tactic:
simp [card]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem coe_zpow (s : Finset α) : ∀ n : ℤ, ↑(s ^ n) = (s : Set α) ^ n
  | Int.ofNat _ => coe_pow _ _
  | Int.negSucc n => by
    refine (coe_inv _).trans ?_
    exact congr_arg Inv.inv (coe_pow _ _)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℕ
⊢ (↑(npowRec n.succ s))⁻¹ = ↑s ^ Int.negSucc n

Tactic:
exact congr_arg Inv.inv (coe_pow _ _)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℕ
⊢ ↑(s ^ Int.negSucc n) = ↑s ^ Int.negSucc n

Tactic:
refine (coe_inv _).trans ?_

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℕ
⊢ (↑(npowRec n.succ s))⁻¹ = ↑s ^ Int.negSucc n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y

Proof state:
⊢ ∀ {x y : Bool}, x ≠ y → x = !y

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
@[to_additive (attr := simp)]
lemma rangeRestrict_injective_iff {f : G →* N} : Injective f.rangeRestrict ↔ Injective f

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ Injective ⇑f.rangeRestrict ↔ Injective ⇑f

Tactic:
convert Set.injective_codRestrict _

Result:
no goals
-- Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
theorem mem_antidiagonalTuple {n : ℕ} {k : ℕ} {x : Fin k → ℕ} :
    x ∈ antidiagonalTuple k n ↔ ∑ i, x i = n

Proof state:
case h0.zero
k : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 0 ↔ ∑ i : Fin 0, i.elim0 = 0

Tactic:
decide

Result:
no goals

Proof state:
case h
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i : Fin n✝, x i = n
n : ℕ
⊢ Fin.cons x₀ x ∈ antidiagonalTuple (n✝ + 1) n ↔ ∑ i : Fin (n✝ + 1), Fin.cons x₀ x i = n

Tactic:
simp_rw [Fin.sum_cons, antidiagonalTuple, List.mem_flatMap, List.mem_map,
  List.Nat.mem_antidiagonal, Fin.cons_inj, exists_eq_right_right, ih,
  @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _),
  ← Prod.mk.inj_iff (a₁ := Prod.fst _), exists_eq_right]

Result:
no goals

Proof state:
case h0
k n : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 n ↔ ∑ i : Fin 0, i.elim0 = n

Tactic:
cases n

Result:
case h0.zero
k : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 0 ↔ ∑ i : Fin 0, i.elim0 = 0

case h0.succ
k n✝ : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 (n✝ + 1) ↔ ∑ i : Fin 0, i.elim0 = n✝ + 1

Proof state:
case h0.succ
k n✝ : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 (n✝ + 1) ↔ ∑ i : Fin 0, i.elim0 = n✝ + 1

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
lemma multinomial_cons (ha : a ∉ s) (f : α → ℕ) :
    multinomial (s.cons a ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f

Proof state:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ multinomial (cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f

Tactic:
rw [multinomial, Nat.div_eq_iff_eq_mul_left _ (prod_factorial_dvd_factorial_sum _ _), prod_cons,
  multinomial, mul_assoc, mul_left_comm _ (f a)!,
  Nat.div_mul_cancel (prod_factorial_dvd_factorial_sum _ _), ← mul_assoc, Nat.choose_symm_add,
  Nat.add_choose_mul_factorial_mul_factorial, Finset.sum_cons]

Result:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ 0 < ∏ i ∈ cons a s ha, (f i)!

Proof state:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ 0 < ∏ i ∈ cons a s ha, (f i)!

Tactic:
positivity

Result:
no goals
-- Mathlib/RingTheory/Frobenius.lean
lemma le_comap : Q ≤ Q.comap φ

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
⊢ Q ≤ Ideal.comap φ Q

Tactic:
intro x hx

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
hx : x ∈ Q
⊢ x ∈ Ideal.comap φ Q

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
hx : x ∈ Q
⊢ x ∈ Ideal.comap φ Q

Tactic:
simp_all only [Ideal.mem_comap, ← Ideal.Quotient.eq_zero_iff_mem (I := Q), H.mk_apply,
  zero_pow_eq, ite_eq_right_iff, H.card_pos.ne', false_implies]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem DFinsupp.sum_inner {ι : Type*} [DecidableEq ι] {α : ι → Type*}
    [∀ i, AddZeroClass (α i)] [∀ (i) (x : α i), Decidable (x ≠ 0)] (f : ∀ i, α i → E)
    (l : Π₀ i, α i) (x : E) : ⟪l.sum f, x⟫ = l.sum fun i a => ⟪f i a, x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
α : ι → Type u_5
inst✝¹ : (i : ι) → AddZeroClass (α i)
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f : (i : ι) → α i → E
l : Π₀ (i : ι), α i
x : E
⊢ ⟪l.sum f, x⟫_𝕜 = l.sum fun i a => ⟪f i a, x⟫_𝕜

Tactic:
simp +contextual only [DFinsupp.sum, sum_inner, smul_eq_mul]

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem Real.coe_fib_eq : ∀ n, (Nat.fib n : ℝ) = (φ ^ n - ψ ^ n) / √5

Proof state:
⊢ ∀ (n : ℕ), ↑(Nat.fib n) = (φ ^ n - ψ ^ n) / √5

Tactic:
rw [← funext_iff, Real.coe_fib_eq']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_def (l : Vector α n) (f : α → Vector β m) : l.flatMap f = flatten (map f l)

Proof state:
α : Type u_1
n : Nat
β : Type u_2
m : Nat
l : Vector α n
f : α → Vector β m
⊢ l.flatMap f = (map f l).flatten

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
m : Nat
f : α → Vector β m
l : Array α
⊢ { toArray := l, size_toArray := ⋯ }.flatMap f = (map f { toArray := l, size_toArray := ⋯ }).flatten

Proof state:
case mk
α : Type u_1
β : Type u_2
m : Nat
f : α → Vector β m
l : Array α
⊢ { toArray := l, size_toArray := ⋯ }.flatMap f = (map f { toArray := l, size_toArray := ⋯ }).flatten

Tactic:
simp [Array.flatMap_def, Function.comp_def]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
@[simp] lemma support_cycleOf_nonempty [DecidableEq α] [Fintype α] :
    (cycleOf f x).support.Nonempty ↔ f x ≠ x

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Nat.succ 0 ≤ #(f.cycleOf x).support ↔ 2 ≤ #(f.cycleOf x).support

Tactic:
exact ⟨fun h => Or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ (f.cycleOf x).support.Nonempty ↔ f x ≠ x

Tactic:
rw [← two_le_card_support_cycleOf_iff, ← card_pos, ← Nat.succ_le_iff]

Result:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Nat.succ 0 ≤ #(f.cycleOf x).support ↔ 2 ≤ #(f.cycleOf x).support
-- Mathlib/CategoryTheory/MorphismProperty/Retract.lean
lemma retracts_monotone : Monotone (retracts (C := C))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone retracts

Tactic:
intro _ _ h _ _ _ ⟨_, _, _, hg, hg'⟩

Result:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝² w✝¹ : C
w✝ : w✝² ⟶ w✝¹
hg : RetractArrow f✝ w✝
hg' : a✝ w✝
⊢ b✝.retracts f✝

Proof state:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝² w✝¹ : C
w✝ : w✝² ⟶ w✝¹
hg : RetractArrow f✝ w✝
hg' : a✝ w✝
⊢ b✝.retracts f✝

Tactic:
exact ⟨_, _, _, hg, h _ hg'⟩

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Algebra.lean
theorem algebraMap_apply (k : R) (a : α) : algebraMap R C(α, A) k a = k • (1 : A)

Proof state:
α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
k : R
a : α
⊢ ((algebraMap R C(α, A)) k) a = k • 1

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Result:
α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
k : R
a : α
⊢ (k • 1) a = k • 1

Proof state:
α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
k : R
a : α
⊢ (k • 1) a = k • 1

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem getElem?_zipWith_eq_some {f : α → β → γ} {l₁ : List α} {l₂ : List β} {z : γ} {i : Nat} :
    (zipWith f l₁ l₂)[i]? = some z ↔
      ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁ : List α
l₂ : List β
z : γ
i : Nat
⊢ (zipWith f l₁ l₂)[i]? = some z ↔ ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Tactic:
induction l₁ generalizing l₂ i

Result:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
l₂ : List β
i : Nat
⊢ (zipWith f [] l₂)[i]? = some z ↔ ∃ x y, [][i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ {l₂ : List β} {i : Nat}, (zipWith f tail✝ l₂)[i]? = some z ↔ ∃ x y, tail✝[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z
l₂ : List β
i : Nat
⊢ (zipWith f (head✝ :: tail✝) l₂)[i]? = some z ↔ ∃ x y, (head✝ :: tail✝)[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ {l₂ : List β} {i : Nat}, (zipWith f tail✝ l₂)[i]? = some z ↔ ∃ x y, tail✝[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z
l₂ : List β
i : Nat
⊢ (zipWith f (head✝ :: tail✝) l₂)[i]? = some z ↔ ∃ x y, (head✝ :: tail✝)[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Tactic:
cases l₂ <;> cases i <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
l₂ : List β
i : Nat
⊢ (zipWith f [] l₂)[i]? = some z ↔ ∃ x y, [][i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivWithinAt.smul_const (hc : HasDerivWithinAt c c' s x) (f : F) :
    HasDerivWithinAt (fun y => c y • f) (c' • f) s x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
f : F
this : HasDerivWithinAt (fun y => c y • f) (c x • 0 + c' • f) s x
⊢ HasDerivWithinAt (fun y => c y • f) (c' • f) s x

Tactic:
rwa [smul_zero, zero_add] at this

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
f : F
⊢ HasDerivWithinAt (fun y => c y • f) (c' • f) s x

Tactic:
have := hc.smul (hasDerivWithinAt_const x s f)

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
f : F
this : HasDerivWithinAt (fun y => c y • f) (c x • 0 + c' • f) s x
⊢ HasDerivWithinAt (fun y => c y • f) (c' • f) s x
-- Mathlib/Topology/AlexandrovDiscrete.lean
lemma closure_sUnion (S : Set (Set α)) : closure (⋃₀ S) = ⋃ s ∈ S, closure s

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
⊢ closure (⋃₀ S) = ⋃ s ∈ S, closure s

Tactic:
simp_rw [sUnion_eq_biUnion, closure_iUnion]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem smul_ball_zero {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} (hk : k ≠ 0) :
    k • p.ball 0 r = p.ball 0 (‖k‖ * r)

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ x✝ ∈ k • p.ball 0 r ↔ x✝ ∈ p.ball 0 (‖k‖ * r)

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hk, p.mem_ball_zero, p.mem_ball_zero, map_smul_eq_mul,
  norm_inv, ← div_eq_inv_mul, div_lt_iff₀ (norm_pos_iff.2 hk), mul_comm]

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
⊢ k • p.ball 0 r = p.ball 0 (‖k‖ * r)

Tactic:
ext

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x✝ : E
⊢ x✝ ∈ k • p.ball 0 r ↔ x✝ ∈ p.ball 0 (‖k‖ * r)
-- Mathlib/Order/Heyting/Basic.lean
theorem le_sup_sdiff_sup_sdiff : a ≤ b ⊔ (a \ c ⊔ c \ b)

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ b ⊔ (a \ c ⊔ c \ b)

Tactic:
simpa using @sdiff_sdiff_sdiff_le_sdiff

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem tendsto_inv_nhdsGE_inv {a : H} : Tendsto Inv.inv (𝓝[≥] a⁻¹) (𝓝[≤] a)

Proof state:
H : Type x
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[≥] a⁻¹) (𝓝[≤] a)

Tactic:
simpa only [inv_inv] using @tendsto_inv_nhdsGE _ _ _ _ a⁻¹

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

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

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

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem maximum_eq_coe_iff : maximum l = m ↔ m ∈ l ∧ ∀ a ∈ l, a ≤ m

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ l.maximum = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m

Tactic:
rw [maximum, ← WithBot.some_eq_coe, argmax_eq_some_iff]

Result:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → idxOf m l ≤ idxOf a l) ↔
    m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ m ∈ l → (∀ (a : α), a ∈ l → a ≤ m) → ∀ (a : α), a ∈ l → m ≤ a → idxOf m l ≤ idxOf a l

Tactic:
intro _ h a hal hma

Result:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
hal : a ∈ l
hma : m ≤ a
⊢ idxOf m l ≤ idxOf a l

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
a✝ : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
hal : a ∈ l
hma : m ≤ a
⊢ idxOf m l ≤ idxOf a l

Tactic:
rw [_root_.le_antisymm hma (h a hal)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → idxOf m l ≤ idxOf a l) ↔
    m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m

Tactic:
simp only [id_eq, and_congr_right_iff, and_iff_left_iff_imp]

Result:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ m ∈ l → (∀ (a : α), a ∈ l → a ≤ m) → ∀ (a : α), a ∈ l → m ≤ a → idxOf m l ≤ idxOf a l
-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
theorem nerve₂Adj.unit.map_app_eq (X : SSet.Truncated.{u} 2) :
    SSet.oneTruncation₂.map (nerve₂Adj.unit.app X) =
    ReflQuiv.adj.{u}.unit.app (SSet.oneTruncation₂.obj X) ⋙rq
    (SSet.Truncated.HomotopyCategory.quotientFunctor X).toReflPrefunctor ⋙rq
    (OneTruncation₂.ofNerve₂.natIso).inv.app (hoFunctor₂.obj X)

Proof state:
X : SSet.Truncated 2
⊢ oneTruncation₂.map (app X) =
    ReflQuiv.adj.unit.app (oneTruncation₂.obj X) ⋙rq (HomotopyCategory.quotientFunctor X).toReflPrefunctor ⋙rq
      OneTruncation₂.ofNerve₂.natIso.inv.app (hoFunctor₂.obj X)

Tactic:
apply oneTruncation₂_toNerve₂Mk'

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem one_le_val_iff (v : Valuation K Γ₀) {x : K} (h : x ≠ 0) : 1 ≤ v x ↔ v x⁻¹ ≤ 1

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x ≠ 0
⊢ 1 ≤ v x ↔ v x⁻¹ ≤ 1

Tactic:
simp [inv_le_one₀ (v.pos_iff.2 h)]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem piIsoPi_hom_apply {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι)
    (x : (∏ᶜ α : TopCat.{max v u})) : (piIsoPi α).hom x i = (Pi.π α i :) x

Proof state:
ι : Type v
α : ι → TopCat
i : ι
x : ↑(∏ᶜ α)
this : (piIsoPi α).inv ≫ Pi.π α i = piπ α i
⊢ (ConcreteCategory.hom (piIsoPi α).hom) x i = (ConcreteCategory.hom (Pi.π α i)) x

Tactic:
rw [Iso.inv_comp_eq] at this

Result:
ι : Type v
α : ι → TopCat
i : ι
x : ↑(∏ᶜ α)
this : Pi.π α i = (piIsoPi α).hom ≫ piπ α i
⊢ (ConcreteCategory.hom (piIsoPi α).hom) x i = (ConcreteCategory.hom (Pi.π α i)) x

Proof state:
ι : Type v
α : ι → TopCat
i : ι
x : ↑(∏ᶜ α)
this : Pi.π α i = (piIsoPi α).hom ≫ piπ α i
⊢ (ConcreteCategory.hom (piIsoPi α).hom) x i = (ConcreteCategory.hom (Pi.π α i)) x

Tactic:
exact ConcreteCategory.congr_hom this x

Result:
no goals

Proof state:
ι : Type v
α : ι → TopCat
i : ι
x : ↑(∏ᶜ α)
⊢ (ConcreteCategory.hom (piIsoPi α).hom) x i = (ConcreteCategory.hom (Pi.π α i)) x

Tactic:
have := piIsoPi_inv_π α i

Result:
ι : Type v
α : ι → TopCat
i : ι
x : ↑(∏ᶜ α)
this : (piIsoPi α).inv ≫ Pi.π α i = piπ α i
⊢ (ConcreteCategory.hom (piIsoPi α).hom) x i = (ConcreteCategory.hom (Pi.π α i)) x
-- Mathlib/Topology/Order/OrderClosed.lean
theorem continuousWithinAt_Ico_iff_Iio (h : a < b) :
    ContinuousWithinAt f (Ico a b) b ↔ ContinuousWithinAt f (Iio b) b

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ico a b) b ↔ ContinuousWithinAt f (Iio b) b

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsLT h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
    [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} :
    ¬ k ∈ m → l.contains k = false →
      getKey? (insertManyIfNewUnit m l) k = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).getKey? k = none

Tactic:
simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ ¬k ∈ m → l.contains k = false → (insertManyIfNewUnit m l).getKey? k = none

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).getKey? k = none
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSub_vadd_affineCombination (w₁ w₂ : ι → k) (p : ι → P) :
    s.weightedVSub p w₁ +ᵥ s.affineCombination k p w₂ = s.affineCombination k p (w₁ + w₂)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → P
⊢ (s.weightedVSub p) w₁ +ᵥ (affineCombination k s p) w₂ = (affineCombination k s p) (w₁ + w₂)

Tactic:
rw [← vadd_eq_add, AffineMap.map_vadd, affineCombination_linear]

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem mem_iInf {ι : Sort*} {S : ι → StarSubalgebra R A} {x : A} :
    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
ι : Sort u_5
S : ι → StarSubalgebra R A
x : A
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem id : IsBoundedLinearMap 𝕜 fun x : E => x :=
  LinearMap.id.isLinear.with_bound 1 <| by simp [le_refl]

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ∀ (x : E), ‖LinearMap.id x‖ ≤ 1 * ‖x‖

Tactic:
simp [le_refl]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma BddAbove.range_mono [Preorder β] {f : α → β} (g : α → β) (h : ∀ a, f a ≤ g a)
    (hbdd : BddAbove (range g)) : BddAbove (range f)

Proof state:
case intro
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
⊢ BddAbove (range f)

Tactic:
use C

Result:
case h
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
⊢ C ∈ upperBounds (range f)

Proof state:
case h
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
⊢ C ∈ upperBounds (range f)

Tactic:
rintro - ⟨x, rfl⟩

Result:
case h.intro
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
x : α
⊢ f x ≤ C

Proof state:
case h.intro
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
x : α
⊢ f x ≤ C

Tactic:
exact (h x).trans (hC <| mem_range_self x)

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
hbdd : BddAbove (range g)
⊢ BddAbove (range f)

Tactic:
obtain ⟨C, hC⟩ := hbdd

Result:
case intro
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
⊢ BddAbove (range f)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insert_self [LawfulBEq α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insert k v).get k (contains_insert_self _ h) = v

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
v : β k
⊢ (m.insert k v).get k ⋯ = v

Tactic:
simp_to_model [insert] using List.getValueCast_insertEntry_self

Result:
no goals
-- Mathlib/Data/Nat/Hyperoperation.lean
theorem hyperoperation_ge_three_eq_one (n m : ℕ) : hyperoperation (n + 3) m 0 = 1

Proof state:
n m : ℕ
⊢ hyperoperation (n + 3) m 0 = 1

Tactic:
rw [hyperoperation]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_comap_comap_eq_relrank_of_surjective
    {L : Type v} [Field L] (f : L →+* E) (h : Function.Surjective f) :
    relrank (A.comap f) (B.comap f) = relrank A B

Proof state:
E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
h : Function.Surjective ⇑f
⊢ (comap f A).relrank (comap f B) = A.relrank B

Tactic:
simpa using lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h

Result:
no goals