harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem coe_sInf (S : Set (Subfield K)) : ((sInf S : Subfield K) : Set K) = ⋂ s ∈ S, ↑s :=
  show ((sInf (Subfield.toSubring '' S) : Subring K) : Set K) = ⋂ s ∈ S, ↑s by
    ext x
    rw [Subring.coe_sInf, Set.mem_iInter, Set.mem_iInter]
    exact
      ⟨fun h s s' ⟨s_mem, s'_eq⟩ => h s.toSubring _ ⟨⟨s, s_mem, rfl⟩, s'_eq⟩,
        fun h s s' ⟨⟨s'', s''_mem, s_eq⟩, (s'_eq : ↑s = s')⟩ =>
        h s'' _ ⟨s''_mem, by simp [← s_eq, ← s'_eq]⟩⟩

Proof state:
case h
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
x : K
⊢ (∀ (i : Subring K), x ∈ ⋂ (_ : i ∈ toSubring '' S), ↑i) ↔ ∀ (i : Subfield K), x ∈ ⋂ (_ : i ∈ S), ↑i

Tactic:
exact
  ⟨fun h s s' ⟨s_mem, s'_eq⟩ => h s.toSubring _ ⟨⟨s, s_mem, rfl⟩, s'_eq⟩,
    fun h s s' ⟨⟨s'', s''_mem, s_eq⟩, (s'_eq : ↑s = s')⟩ =>
    h s'' _ ⟨s''_mem, by simp [← s_eq, ← s'_eq]⟩⟩

Result:
no goals

Proof state:
case h
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
x : K
⊢ x ∈ ↑(sInf (toSubring '' S)) ↔ x ∈ ⋂ s ∈ S, ↑s

Tactic:
rw [Subring.coe_sInf, Set.mem_iInter, Set.mem_iInter]

Result:
case h
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
x : K
⊢ (∀ (i : Subring K), x ∈ ⋂ (_ : i ∈ toSubring '' S), ↑i) ↔ ∀ (i : Subfield K), x ∈ ⋂ (_ : i ∈ S), ↑i

Proof state:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
x : K
h : ∀ (i : Subfield K), x ∈ ⋂ (_ : i ∈ S), ↑i
s : Subring K
s' : Set K
x✝ : s' ∈ Set.range fun h => ↑s
s'' : Subfield K
s''_mem : s'' ∈ S
s_eq : s''.toSubring = s
s'_eq : ↑s = s'
⊢ (fun h => ↑s'') s''_mem = s'

Tactic:
simp [← s_eq, ← s'_eq]

Result:
no goals

Proof state:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
⊢ ↑(sInf (toSubring '' S)) = ⋂ s ∈ S, ↑s

Tactic:
ext x

Result:
case h
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
x : K
⊢ x ∈ ↑(sInf (toSubring '' S)) ↔ x ∈ ⋂ s ∈ S, ↑s
-- Mathlib/Data/Real/Irrational.lean
theorem rat_sub (h : Irrational x) : Irrational (q - x)

Proof state:
q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (↑q - x)

Tactic:
simpa only [sub_eq_add_neg] using h.neg.rat_add q

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem edgeFinset_subset_edgeFinset : G₁.edgeFinset ⊆ G₂.edgeFinset ↔ G₁ ≤ G₂

Proof state:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ G₁.edgeFinset ⊆ G₂.edgeFinset ↔ G₁ ≤ G₂

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapHomologyIso'_inv_naturality [S₁.HasHomology] [S₂.HasHomology]
    [(S₁.map F).HasHomology] [(S₂.map F).HasHomology]
    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
    F.map (homologyMap φ) ≫ (S₂.mapHomologyIso' F).inv = (S₁.mapHomologyIso' F).inv ≫
      @homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} C
inst✝⁹ : Category.{u_4, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ F.map (homologyMap φ) ≫ (S₂.mapHomologyIso' F).inv =
    (S₁.mapHomologyIso' F).inv ≫ homologyMap (F.mapShortComplex.map φ)

Tactic:
rw [← cancel_epi (S₁.mapHomologyIso' F).hom, ← mapHomologyIso'_hom_naturality_assoc,
  Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_map (p : β → Bool) (f : α → β) :
    ∀ l, countP p (map f l) = countP (p ∘ f) l
  | [] => rfl
  | a :: l => by rw [map_cons, countP_cons, countP_cons, countP_map p f l]; rfl

Proof state:
α : Type u_2
β : Type u_1
p : β → Bool
f : α → β
a : α
l : List α
⊢ (countP (p ∘ f) l + if p (f a) = true then 1 else 0) = countP (p ∘ f) l + if (p ∘ f) a = true then 1 else 0

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
p : β → Bool
f : α → β
a : α
l : List α
⊢ countP p (map f (a :: l)) = countP (p ∘ f) (a :: l)

Tactic:
rw [map_cons, countP_cons, countP_cons, countP_map p f l]

Result:
α : Type u_2
β : Type u_1
p : β → Bool
f : α → β
a : α
l : List α
⊢ (countP (p ∘ f) l + if p (f a) = true then 1 else 0) = countP (p ∘ f) l + if (p ∘ f) a = true then 1 else 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.lo_eq_true_of_lo (u v k₁ k₂ : Nat) : isLE k₂ k₁ = true → u + k₁ ≤ v → (u + k₂ ≤ v) = True :=
  by simp [isLt]; omega

Proof state:
u v k₁ k₂ : Nat
⊢ k₂ ≤ k₁ → u + k₁ ≤ v → u + k₂ ≤ v

Tactic:
omega

Result:
no goals

Proof state:
u v k₁ k₂ : Nat
⊢ isLE k₂ k₁ = true → u + k₁ ≤ v → (u + k₂ ≤ v) = True

Tactic:
simp [isLt]

Result:
u v k₁ k₂ : Nat
⊢ k₂ ≤ k₁ → u + k₁ ≤ v → u + k₂ ≤ v
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
lemma orthogonal_orthogonal (hB : B.Nondegenerate) (hB₀ : B.IsRefl) (W : Submodule K V) :
    B.orthogonal (B.orthogonal W) = W

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
⊢ finrank K V - (finrank K V - finrank K ↥W) ≤ finrank K ↥W

Tactic:
omega

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
⊢ B.orthogonal (B.orthogonal W) = W

Tactic:
apply (eq_of_le_of_finrank_le (LinearMap.BilinForm.le_orthogonal_orthogonal hB₀) _).symm

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
⊢ finrank K ↥(B.orthogonal (B.orthogonal W)) ≤ finrank K ↥W

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
⊢ finrank K ↥(B.orthogonal (B.orthogonal W)) ≤ finrank K ↥W

Tactic:
simp only [finrank_orthogonal hB hB₀]

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
⊢ finrank K V - (finrank K V - finrank K ↥W) ≤ finrank K ↥W
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma mabs_le_mabs_of_le_one (ha : a ≤ 1) (hab : b ≤ a) : |a|ₘ ≤ |b|ₘ

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ a⁻¹ ≤ b⁻¹

Tactic:
exact inv_le_inv_iff.mpr hab

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ mabs a ≤ mabs b

Tactic:
rw [mabs_of_le_one ha, mabs_of_le_one (hab.trans ha)]

Result:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ a⁻¹ ≤ b⁻¹
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nadd_le_nadd_right (h : b ≤ c) (a) : b ♯ a ≤ c ♯ a

Proof state:
b c : Ordinal.{u}
h : b ≤ c
a : Ordinal.{u}
⊢ b ♯ a ≤ c ♯ a

Tactic:
rcases lt_or_eq_of_le h with (h | rfl)

Result:
case inl
b c : Ordinal.{u}
h✝ : b ≤ c
a : Ordinal.{u}
h : b < c
⊢ b ♯ a ≤ c ♯ a

case inr
b a : Ordinal.{u}
h : b ≤ b
⊢ b ♯ a ≤ b ♯ a

Proof state:
case inr
b a : Ordinal.{u}
h : b ≤ b
⊢ b ♯ a ≤ b ♯ a

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case inl
b c : Ordinal.{u}
h✝ : b ≤ c
a : Ordinal.{u}
h : b < c
⊢ b ♯ a ≤ c ♯ a

Tactic:
exact (nadd_lt_nadd_right h a).le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_sub (n m k : Nat) : n - m - k = n - (m + k)

Proof state:
case succ
n m k : Nat
ih : n - m - k = n - (m + k)
⊢ n - m - (k + 1) = n - (m + (k + 1))

Tactic:
rw [Nat.add_succ, Nat.sub_succ, Nat.add_succ, Nat.sub_succ, ih]

Result:
no goals

Proof state:
n m k : Nat
⊢ n - m - k = n - (m + k)

Tactic:
induction k with
| zero => simp
| succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.add_succ, Nat.sub_succ, ih]

Result:
no goals

Proof state:
case zero
n m : Nat
⊢ n - m - 0 = n - (m + 0)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_add_Ioc : (fun x => a + x) ⁻¹' Ioc b c = Ioc (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Ioc b c = Ioc (b - a) (c - a)

Tactic:
simp [← Ioi_inter_Iic]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HomeomorphBall.lean
theorem continuous_univBall (c : P) (r : ℝ) : Continuous (univBall c r)

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ Continuous ↑(univBall c r)

Tactic:
simpa [continuous_iff_continuousOn_univ] using (univBall c r).continuousOn

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem le_tsum_condensed (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) :
    ∑' k, f k ≤ f 0 + ∑' k : ℕ, 2 ^ k * f (2 ^ k)

Proof state:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ x ∈ range n, 2 ^ x * f (2 ^ x) ≤ ∑' (x : ℕ), 2 ^ x * f (2 ^ x)

Tactic:
apply ENNReal.sum_le_tsum

Result:
no goals

Proof state:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ⨆ i, ∑ a ∈ range (2 ^ i), f a ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)

Tactic:
refine iSup_le fun n => (Finset.le_sum_condensed hf n).trans (add_le_add_left ?_ _)

Result:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range n, 2 ^ k • f (2 ^ k) ≤ ∑' (k : ℕ), 2 ^ k * f (2 ^ k)

Proof state:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)

Tactic:
rw [ENNReal.tsum_eq_iSup_nat' (Nat.tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)]

Result:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ⨆ i, ∑ a ∈ range (2 ^ i), f a ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)

Proof state:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range n, 2 ^ k • f (2 ^ k) ≤ ∑' (k : ℕ), 2 ^ k * f (2 ^ k)

Tactic:
simp only [nsmul_eq_mul, Nat.cast_pow, Nat.cast_two]

Result:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ x ∈ range n, 2 ^ x * f (2 ^ x) ≤ ∑' (x : ℕ), 2 ^ x * f (2 ^ x)
-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
/-- A convenience constructor for `HasAffineProperty P (affineAnd Q)`. The `IsAffineHom` is bundled,
since this goes well with defining morphism properties via `extends IsAffineHom`. -/
lemma HasAffineProperty.affineAnd_iff (P : MorphismProperty Scheme.{u})
    (hQi : RingHom.RespectsIso Q) (hQl : RingHom.LocalizationAwayPreserves Q)
    (hQs : RingHom.OfLocalizationSpan Q) :
    HasAffineProperty P (affineAnd Q) ↔
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y), P f ↔
        (IsAffineHom f ∧ ∀ U : Y.Opens, IsAffineOpen U → Q (f.app U).hom)

Proof state:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q
h : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]

Result:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q
h : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Proof state:
case refine_2.h
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
X Y : Scheme
f : X ⟶ Y
⊢ ((∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Iic_mul_Iio_subset' [LocallyFiniteOrderBot α] (a b : α) : Iic a * Iio b ⊆ Iio (a * b) :=
  Finset.coe_subset.mp <| by simpa using Set.Iic_mul_Iio_subset' _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ ↑(Iic a * Iio b) ⊆ ↑(Iio (a * b))

Tactic:
simpa using Set.Iic_mul_Iio_subset' _ _

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem span_pow (s : Set A) : ∀ n : ℕ, span R s ^ n = span R (s ^ n)
  | 0 => by rw [pow_zero, pow_zero, one_eq_span_one_set]
  | n + 1 => by rw [pow_succ, pow_succ, span_pow s n, span_mul_span]

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ span R s ^ 0 = span R (s ^ 0)

Tactic:
rw [pow_zero, pow_zero, one_eq_span_one_set]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
n : ℕ
⊢ span R s ^ (n + 1) = span R (s ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, span_pow s n, span_mul_span]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_iInf_right [Nonempty ι] {f : Filter α} {g : ι → Filter β} :
    (f ×ˢ ⨅ i, g i) = ⨅ i, f ×ˢ g i

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
f : Filter α
g : ι → Filter β
⊢ f ×ˢ ⨅ i, g i = ⨅ i, f ×ˢ g i

Tactic:
simp only [prod_eq_inf, comap_iInf, inf_iInf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_ofList_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')]
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (ofList l).get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (ofList l).get! k' = cast ⋯ v

Tactic:
simp_to_raw using Raw₀.get!_insertMany_empty_list_of_mem

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
case e_a
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem tendsto_measure_iInter_atTop [Preorder ι]
    [IsCountablyGenerated (atTop : Filter ι)] {s : ι → Set α}
    (hs : ∀ i, NullMeasurableSet (s i) μ) (hm : Antitone s) (hf : ∃ i, μ (s i) ≠ ∞) :
    Tendsto (μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ⊤
h : atTop.NeBot
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))

Tactic:
have := (atTop_neBot_iff.1 h).2

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ⊤
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ⊤
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (⨅ i, μ (s i)))

Tactic:
exact tendsto_atTop_iInf fun n m hnm => measure_mono <| hm hnm

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ⊤
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))

Tactic:
refine .of_neBot_imp fun h ↦ ?_

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ⊤
h : atTop.NeBot
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ⊤
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋂ n, s n)))

Tactic:
rw [hm.measure_iInter hs hf]

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ⊤
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (⨅ i, μ (s i)))
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem absNorm_span_insert (r : S) (s : Set S) :
    absNorm (span (insert r s)) ∣ gcd (absNorm (span s)) (Algebra.norm ℤ r).natAbs :=
  (dvd_gcd_iff _ _ _).mpr
    ⟨absNorm_dvd_absNorm_of_le (span_mono (Set.subset_insert _ _)),
      _root_.trans
        (absNorm_dvd_absNorm_of_le (span_mono (Set.singleton_subset_iff.mpr (Set.mem_insert _ _))))
        (by rw [absNorm_span_singleton])⟩

Proof state:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
r : S
s : Set S
⊢ absNorm (span {r}) ∣ ((Algebra.norm ℤ) r).natAbs

Tactic:
rw [absNorm_span_singleton]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_eq_asc_factorial_div_factorial (n k : ℕ) :
    (n + k).choose k = (n + 1).ascFactorial k / k !

Proof state:
n k : ℕ
⊢ k ! * (n + k).choose k = k ! * ((n + 1).ascFactorial k / k !)

Tactic:
rw [← ascFactorial_eq_factorial_mul_choose]

Result:
n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)

Proof state:
n k : ℕ
⊢ (n + k).choose k = (n + 1).ascFactorial k / k !

Tactic:
apply Nat.mul_left_cancel k.factorial_pos

Result:
n k : ℕ
⊢ k ! * (n + k).choose k = k ! * ((n + 1).ascFactorial k / k !)

Proof state:
n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)

Tactic:
exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Expand.lean
theorem expand_one : expand 1 = AlgHom.id R (MvPolynomial σ R)

Proof state:
case hf
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : σ
⊢ (expand 1) (X f) = (AlgHom.id R (MvPolynomial σ R)) (X f)

Tactic:
rw [expand_one_apply, AlgHom.id_apply]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ expand 1 = AlgHom.id R (MvPolynomial σ R)

Tactic:
ext1 f

Result:
case hf
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : σ
⊢ (expand 1) (X f) = (AlgHom.id R (MvPolynomial σ R)) (X f)
-- Mathlib/Topology/ContinuousOn.lean
lemma Continuous.tendsto_nhdsSet_nhds
    {b : β} {f : α → β} (h : Continuous f) (h' : EqOn f (fun _ ↦ b) s) :
    Tendsto f (𝓝ˢ s) (𝓝 b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous f
h' : EqOn f (fun x => b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ {b})

Tactic:
exact h.tendsto_nhdsSet h'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous f
h' : EqOn f (fun x => b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝 b)

Tactic:
rw [← nhdsSet_singleton]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous f
h' : EqOn f (fun x => b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ {b})
-- Mathlib/Topology/Algebra/Valued/NormedValued.lean
theorem norm_nonneg (x : L) : 0 ≤ norm x

Proof state:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
⊢ 0 ≤ norm x

Tactic:
simp only [norm, NNReal.zero_le_coe]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem lintegral_mono_measure {f : α →ₛ ℝ≥0∞} (h : μ ≤ ν) : f.lintegral μ ≤ f.lintegral ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
h : μ ≤ ν
⊢ f.lintegral μ ≤ f.lintegral ν

Tactic:
simp only [lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
h : μ ≤ ν
⊢ ∑ x ∈ f.range, x * μ (⇑f ⁻¹' {x}) ≤ ∑ x ∈ f.range, x * ν (⇑f ⁻¹' {x})

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
h : μ ≤ ν
⊢ ∑ x ∈ f.range, x * μ (⇑f ⁻¹' {x}) ≤ ∑ x ∈ f.range, x * ν (⇑f ⁻¹' {x})

Tactic:
gcongr

Result:
case h.bc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
h : μ ≤ ν
i✝ : ℝ≥0∞
a✝ : i✝ ∈ f.range
⊢ μ (⇑f ⁻¹' {i✝}) ≤ ν (⇑f ⁻¹' {i✝})

Proof state:
case h.bc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
h : μ ≤ ν
i✝ : ℝ≥0∞
a✝ : i✝ ∈ f.range
⊢ μ (⇑f ⁻¹' {i✝}) ≤ ν (⇑f ⁻¹' {i✝})

Tactic:
apply h

Result:
no goals