harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem nhds_basis_closed_balanced [RegularSpace E] :
    (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E) ∧ IsClosed s ∧ Balanced 𝕜 s) id

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NormedDivisionRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
s : Set E
hs : s ∈ 𝓝 0 ∧ IsClosed s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ IsClosed i' ∧ Balanced 𝕜 i') ∧ id i' ⊆ id s

Tactic:
refine ⟨balancedCore 𝕜 s, ⟨balancedCore_mem_nhds_zero hs.1, ?_⟩, balancedCore_subset s⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NormedDivisionRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
s : Set E
hs : s ∈ 𝓝 0 ∧ IsClosed s
⊢ IsClosed (balancedCore 𝕜 s) ∧ Balanced 𝕜 (balancedCore 𝕜 s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NormedDivisionRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
⊢ (𝓝 0).HasBasis (fun s => s ∈ 𝓝 0 ∧ IsClosed s ∧ Balanced 𝕜 s) id

Tactic:
refine
  (closed_nhds_basis 0).to_hasBasis (fun s hs => ?_) fun s hs => ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NormedDivisionRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
s : Set E
hs : s ∈ 𝓝 0 ∧ IsClosed s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ IsClosed i' ∧ Balanced 𝕜 i') ∧ id i' ⊆ id s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NormedDivisionRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
s : Set E
hs : s ∈ 𝓝 0 ∧ IsClosed s
⊢ IsClosed (balancedCore 𝕜 s) ∧ Balanced 𝕜 (balancedCore 𝕜 s)

Tactic:
exact ⟨hs.2.balancedCore, balancedCore_balanced s⟩

Result:
no goals
-- Mathlib/Data/Set/Image.lean
lemma Codisjoint.preimage (f : α → β) {s t : Set β} (h : Codisjoint s t) :
    Codisjoint (f ⁻¹' s) (f ⁻¹' t)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ∪ t = ⊤
⊢ f ⁻¹' (s ∪ t) = ⊤

Tactic:
rw [h]

Result:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ∪ t = ⊤
⊢ f ⁻¹' ⊤ = ⊤

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : Codisjoint s t
⊢ Codisjoint (f ⁻¹' s) (f ⁻¹' t)

Tactic:
simp only [codisjoint_iff_le_sup, Set.sup_eq_union, top_le_iff, ← Set.preimage_union] at h ⊢

Result:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ∪ t = ⊤
⊢ f ⁻¹' (s ∪ t) = ⊤

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ∪ t = ⊤
⊢ f ⁻¹' ⊤ = ⊤

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem smul_get (xs : IntList) (a : Int) (i : Nat) : (a * xs).get i = a * xs.get i

Proof state:
xs : IntList
a : Int
i : Nat
⊢ (Option.map (fun x => a * x) xs[i]?).getD 0 = a * xs[i]?.getD 0

Tactic:
cases xs[i]? <;> simp

Result:
no goals

Proof state:
xs : IntList
a : Int
i : Nat
⊢ (a * xs).get i = a * xs.get i

Tactic:
simp only [get, smul_def, List.get?_eq_getElem?, List.getElem?_map]

Result:
xs : IntList
a : Int
i : Nat
⊢ (Option.map (fun x => a * x) xs[i]?).getD 0 = a * xs[i]?.getD 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bdiv_add_bmod' (x : Int) (m : Nat) : bdiv x m * m + bmod x m = x

Proof state:
x : Int
m : Nat
⊢ x.bdiv m * ↑m + x.bmod m = x

Tactic:
rw [Int.mul_comm]

Result:
x : Int
m : Nat
⊢ ↑m * x.bdiv m + x.bmod m = x

Proof state:
x : Int
m : Nat
⊢ ↑m * x.bdiv m + x.bmod m = x

Tactic:
exact bdiv_add_bmod x m

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_lt_opow_left_of_succ {a b c : Ordinal} (ab : a < b) : a ^ succ c < b ^ succ c

Proof state:
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ succ c < b ^ succ c

Tactic:
rw [opow_succ, opow_succ]

Result:
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c * a < b ^ c * b

Proof state:
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c * a < b ^ c * b

Tactic:
exact
  (mul_le_mul_right' (opow_le_opow_left c ab.le) a).trans_lt
    (mul_lt_mul_of_pos_left ab (opow_pos c ((Ordinal.zero_le a).trans_lt ab)))

Result:
no goals
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive] lemma mulEnergy_eq_sum_sq [Fintype α] (s t : Finset α) :
    Eₘ[s, t] = ∑ a, ((s ×ˢ t).filter fun (x, y) ↦ x * y = a).card ^ 2

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Mul α
inst✝ : Fintype α
s t : Finset α
⊢ ∑ a ∈ s * t,
      #(filter
            (fun x =>
              match x with
              | (x, y) => x * y = a)
            (s ×ˢ t)) ^
        2 =
    ∑ a : α,
      #(filter
            (fun x =>
              match x with
              | (x, y) => x * y = a)
            (s ×ˢ t)) ^
        2

Tactic:
exact Fintype.sum_subset <| by aesop (add simp [filter_eq_empty_iff, mul_mem_mul])

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Mul α
inst✝ : Fintype α
s t : Finset α
⊢ Eₘ[s, t] =
    ∑ a : α,
      #(filter
            (fun x =>
              match x with
              | (x, y) => x * y = a)
            (s ×ˢ t)) ^
        2

Tactic:
rw [mulEnergy_eq_sum_sq']

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Mul α
inst✝ : Fintype α
s t : Finset α
⊢ ∑ a ∈ s * t,
      #(filter
            (fun x =>
              match x with
              | (x, y) => x * y = a)
            (s ×ˢ t)) ^
        2 =
    ∑ a : α,
      #(filter
            (fun x =>
              match x with
              | (x, y) => x * y = a)
            (s ×ˢ t)) ^
        2

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Mul α
inst✝ : Fintype α
s t : Finset α
⊢ ∀ (i : α),
    #(filter
              (fun x =>
                match x with
                | (x, y) => x * y = i)
              (s ×ˢ t)) ^
          2 ≠
        0 →
      i ∈ s * t

Tactic:
aesop (add simp [filter_eq_empty_iff, mul_mem_mul])

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
@[simp] lemma isSymmSndFDerivWithinAt_univ :
    IsSymmSndFDerivWithinAt 𝕜 f univ x ↔ IsSymmSndFDerivAt 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ x ↔ IsSymmSndFDerivAt 𝕜 f x

Tactic:
simp [IsSymmSndFDerivWithinAt, IsSymmSndFDerivAt]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem inl_snd' {b : BinaryBicone X Y} (h : b.IsBilimit) :
    IsPushout b.inl (0 : X ⟶ 0) b.snd (0 : 0 ⟶ Y)

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout (0 ≫ 0) 0 0 (b.inr ≫ b.snd)

Tactic:
simp

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout 0 b.inl 0 b.snd

Tactic:
refine of_left ?_ (by simp) (of_isBilimit h)

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout (0 ≫ 0) 0 0 (b.inr ≫ b.snd)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout b.inl 0 b.snd 0

Tactic:
apply flip

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout 0 b.inl 0 b.snd

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 ≫ 0 = b.inl ≫ b.snd

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
@[simp]
lemma restrict_id (f : X.PartialMap Y) : f.restrict f.domain f.dense_domain le_rfl = f

Proof state:
X Y : Scheme
f : X.PartialMap Y
⊢ f.restrict f.domain ⋯ ⋯ = f

Tactic:
ext1 <;> simp [restrict_domain]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem extend_eq_top {s : α} (h : ¬P s) : extend m s = ∞

Proof state:
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : ¬P s
⊢ extend m s = ⊤

Tactic:
simp [extend, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_mul {x : BitVec w} : 0#w * x = 0#w

Proof state:
case a
w : Nat
x : BitVec w
⊢ (0#w * x).toNat = (0#w).toNat

Tactic:
simp [toNat_mul]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ 0#w * x = 0#w

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
x : BitVec w
⊢ (0#w * x).toNat = (0#w).toNat
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem ciSup_le [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, f x ≤ c) : iSup f ≤ c :=
  csSup_le (range_nonempty f) (by rwa [forall_mem_range])

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
c : α
H : ∀ (x : ι), f x ≤ c
⊢ ∀ b ∈ range f, b ≤ c

Tactic:
rwa [forall_mem_range]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma homologyMap_nullHomotopic [S₁.HasHomology] [S₂.HasHomology]
    (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : h₀ ≫ S₂.f = 0)
    (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : S₁.g ≫ h₃ = 0) :
    homologyMap (nullHomotopic _ _ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ homologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

Tactic:
apply homologyMap'_nullHomotopic

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem cast_le_intCast {m : ℚ} {n : ℤ} : (m : K) ≤ n ↔ m ≤ (n : ℚ)

Proof state:
K : Type u_5
inst✝ : LinearOrderedField K
m : ℚ
n : ℤ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
rw [← cast_le (K := K), cast_intCast]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/InfiniteSum.lean
theorem cauchySeq_range_of_norm_bounded {f : ℕ → E} (g : ℕ → ℝ)
    (hg : CauchySeq fun n => ∑ i ∈ range n, g i) (hf : ∀ i, ‖f i‖ ≤ g i) :
    CauchySeq fun n => ∑ i ∈ range n, f i

Proof state:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq fun n => ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
⊢ CauchySeq fun n => ∑ i ∈ range n, f i

Tactic:
refine Metric.cauchySeq_iff'.2 fun ε hε => ?_

Result:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq fun n => ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε

Proof state:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : dist (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε
⊢ dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε

Tactic:
rw [dist_eq_norm, ← sum_Ico_eq_sub _ hn] at hg ⊢

Result:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : ‖∑ k ∈ Ico N n, g k‖ < ε
⊢ ‖∑ k ∈ Ico N n, f k‖ < ε

Proof state:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : ‖∑ k ∈ Ico N n, g k‖ < ε
⊢ ‖∑ k ∈ Ico N n, f k‖ < ε

Tactic:
calc
  ‖∑ k ∈ Ico N n, f k‖ ≤ ∑ k ∈ _, ‖f k‖ := norm_sum_le _ _
  _ ≤ ∑ k ∈ _, g k := sum_le_sum fun x _ => hf x
  _ ≤ ‖∑ k ∈ _, g k‖ := le_abs_self _
  _ < ε := hg

Result:
no goals

Proof state:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq fun n => ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε

Tactic:
refine (Metric.cauchySeq_iff'.1 hg ε hε).imp fun N hg n hn => ?_

Result:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N : ℕ
hg : ∀ n ≥ N, dist (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε
n : ℕ
hn : n ≥ N
⊢ dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε

Proof state:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N : ℕ
hg : ∀ n ≥ N, dist (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε
n : ℕ
hn : n ≥ N
⊢ dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε

Tactic:
specialize hg n hn

Result:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : dist (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε
⊢ dist (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_eq_image_lineMap (x y : E) :
    openSegment 𝕜 x y = AffineMap.lineMap x y '' Ioo (0 : 𝕜) 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
⊢ openSegment 𝕜 x y = ⇑(AffineMap.lineMap x y) '' Ioo 0 1

Tactic:
convert openSegment_eq_image 𝕜 x y using 2

Result:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ (AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y

Proof state:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ (AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y

Tactic:
exact AffineMap.lineMap_apply_module _ _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/OfFn.lean
theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ i, f i = a

Proof state:
case mpr
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → a ∈ ofFn f

Tactic:
rintro ⟨i, rfl⟩

Result:
case mpr.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Fin n
⊢ f i ∈ ofFn f

Proof state:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
w : a ∈ ofFn f
⊢ ∃ i, f i = a

Tactic:
obtain ⟨i, h, rfl⟩ := getElem_of_mem w

Result:
case mp.intro.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < (ofFn f).size
w : (ofFn f)[i] ∈ ofFn f
⊢ ∃ i_1, f i_1 = (ofFn f)[i]

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < (ofFn f).size
w : (ofFn f)[i] ∈ ofFn f
⊢ i < n

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ ∃ i, f i = a

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f → ∃ i, f i = a

case mpr
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → a ∈ ofFn f

Proof state:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f → ∃ i, f i = a

Tactic:
intro w

Result:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
w : a ∈ ofFn f
⊢ ∃ i, f i = a

Proof state:
case mpr.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Fin n
⊢ f i ∈ ofFn f

Tactic:
apply mem_of_getElem (i := i) <;> simp

Result:
no goals

Proof state:
case mp.intro.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < (ofFn f).size
w : (ofFn f)[i] ∈ ofFn f
⊢ ∃ i_1, f i_1 = (ofFn f)[i]

Tactic:
exact ⟨⟨i, by simpa using h⟩, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < (ofFn f).size
w : (ofFn f)[i] ∈ ofFn f
⊢ f ⟨i, ⋯⟩ = (ofFn f)[i]

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_neg : ∀ x : PGame, (-x).birthday = x.birthday
  | ⟨xl, xr, xL, xR⟩ => by
    rw [birthday_def, birthday_def, max_comm]
    congr <;> funext <;> apply birthday_neg

Proof state:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ (-mk xl xr xL xR).birthday = (mk xl xr xL xR).birthday

Tactic:
rw [birthday_def, birthday_def, max_comm]

Result:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ ((lsub fun i => ((-mk xl xr xL xR).moveRight i).birthday) ⊔ lsub fun i => ((-mk xl xr xL xR).moveLeft i).birthday) =
    (lsub fun i => ((mk xl xr xL xR).moveLeft i).birthday) ⊔ lsub fun i => ((mk xl xr xL xR).moveRight i).birthday

Proof state:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ ((lsub fun i => ((-mk xl xr xL xR).moveRight i).birthday) ⊔ lsub fun i => ((-mk xl xr xL xR).moveLeft i).birthday) =
    (lsub fun i => ((mk xl xr xL xR).moveLeft i).birthday) ⊔ lsub fun i => ((mk xl xr xL xR).moveRight i).birthday

Tactic:
congr <;> funext <;> apply birthday_neg

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem ncard_block_mul_ncard_orbit_eq (hB : IsBlock G B) (hB_ne : B.Nonempty) :
    Set.ncard B * Set.ncard (orbit G B) = Nat.card X

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : B.Nonempty
⊢ B.ncard * (orbit G B).ncard = Nat.card X

Tactic:
obtain ⟨x, hx⟩ := hB_ne

Result:
case intro
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ B.ncard * (orbit G B).ncard = Nat.card X

Proof state:
case intro
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ B.ncard * (orbit G B).ncard = Nat.card X

Tactic:
rw [ncard_block_eq_relindex hB hx, ← index_stabilizer,
    Subgroup.relindex_mul_index (hB.stabilizer_le hx), index_stabilizer_of_transitive]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
@[simp]
protected lemma add_add_tsub_cancel (hc : AddLECancellable c) (hcb : c ≤ b) :
    a + c + (b - c) = a + b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
hcb : c ≤ b
⊢ a + c + (b - c) = a + b

Tactic:
rw [← hc.add_tsub_assoc_of_le hcb, add_right_comm, hc.add_tsub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem lt_of_tsub_lt_tsub_left_of_le [AddLeftReflectLT α]
    (hb : AddLECancellable b) (hca : c ≤ a) (h : a - b < a - c) : c < b

Proof state:
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
⊢ c < b

Tactic:
conv_lhs at h => rw [← tsub_add_cancel_of_le hca]

Result:
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - c + c - b < a - c
⊢ c < b

Proof state:
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - c + c - b < a - c
⊢ c < b

Tactic:
exact lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_add : (p + q).support ⊆ p.support ∪ q.support

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p + q).support ⊆ p.support ∪ q.support

Tactic:
simpa [support] using Finsupp.support_add

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem smul_unitBall_of_pos {r : ℝ} (hr : 0 < r) : r • ball (0 : E) 1 = ball (0 : E) r

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
⊢ r • ball 0 1 = ball 0 r

Tactic:
rw [smul_unitBall hr.ne', Real.norm_of_nonneg hr.le]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma mem_comap {I : TwoSidedIdeal S} {x : R} :
    x ∈ I.comap f ↔ f x ∈ I

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
I : TwoSidedIdeal S
x : R
⊢ x ∈ (comap f) I ↔ f x ∈ I

Tactic:
simp [comap, RingCon.comap, mem_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem hasSum_integral_of_dominated_convergence {ι} [Countable ι] {F : ι → ℝ → E}
    (bound : ι → ℝ → ℝ) (hF_meas : ∀ n, AEStronglyMeasurable (F n) (μ.restrict (Ι a b)))
    (h_bound : ∀ n, ∀ᵐ t ∂μ, t ∈ Ι a b → ‖F n t‖ ≤ bound n t)
    (bound_summable : ∀ᵐ t ∂μ, t ∈ Ι a b → Summable fun n => bound n t)
    (bound_integrable : IntervalIntegrable (fun t => ∑' n, bound n t) μ a b)
    (h_lim : ∀ᵐ t ∂μ, t ∈ Ι a b → HasSum (fun n => F n t) (f t)) :
    HasSum (fun n => ∫ t in a..b, F n t ∂μ) (∫ t in a..b, f t ∂μ)

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
inst✝ : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ (n : ι), ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound n x
bound_summable : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Summable fun n => bound n x
bound_integrable : IntegrableOn (fun t => ∑' (n : ι), bound n t) (Ι a b) μ
h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasSum (fun n => F n x) (f x)
⊢ HasSum (fun n => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F n t ∂μ)
    ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, f t ∂μ)

Tactic:
exact
  (hasSum_integral_of_dominated_convergence bound hF_meas h_bound bound_summable bound_integrable
        h_lim).const_smul
    _

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
inst✝ : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F n t‖ ≤ bound n t
bound_summable : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Summable fun n => bound n t
bound_integrable : IntervalIntegrable (fun t => ∑' (n : ι), bound n t) μ a b
h_lim : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasSum (fun n => F n t) (f t)
⊢ HasSum (fun n => ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)

Tactic:
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc, ←
  ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *

Result:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
inst✝ : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ (n : ι), ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound n x
bound_summable : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Summable fun n => bound n x
bound_integrable : IntegrableOn (fun t => ∑' (n : ι), bound n t) (Ι a b) μ
h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasSum (fun n => F n x) (f x)
⊢ HasSum (fun n => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F n t ∂μ)
    ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, f t ∂μ)
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_mul_mulInv_mul (A B C : Finset G) :
    #B * #(A * C) ≤ #(B * A⁻¹) * #(B * C)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A * C) ≤ #(B * A⁻¹) * #(B * C)

Tactic:
simpa [div_eq_mul_inv] using ruzsa_triangle_inequality_mul_div_mul A B C

Result:
no goals
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_trailingCoeff : p.mirror.trailingCoeff = p.leadingCoeff

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.mirror.trailingCoeff = p.leadingCoeff

Tactic:
rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror,
  revAt_le (Nat.le_add_left _ _), add_tsub_cancel_right]

Result:
no goals