harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Chain.lean
theorem Chain'.induction (p : α → Prop) (l : List α) (h : Chain' r l)
    (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : (lne : l ≠ []) → p (l.head lne)) :
    ∀ i ∈ l, p i

Proof state:
case h_2
α : Type u
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
x✝ : List α
a✝ : α
l✝ : List α
initial : p a✝
h : Chain r a✝ l✝
⊢ ∀ (a : α), a ∈ l✝ → p a

Tactic:
exact h.induction p _ carries initial

Result:
no goals

Proof state:
case h_2
α : Type u
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
x✝ : List α
a✝ : α
l✝ : List α
initial : ∀ (lne : a✝ :: l✝ ≠ []), p ((a✝ :: l✝).head lne)
h : Chain r a✝ l✝
⊢ ∀ (i : α), i ∈ a✝ :: l✝ → p i

Tactic:
simp_all only [ne_eq, not_false_eq_true, head_cons, true_implies, mem_cons, forall_eq_or_imp,
  true_and, reduceCtorEq]

Result:
case h_2
α : Type u
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
x✝ : List α
a✝ : α
l✝ : List α
initial : p a✝
h : Chain r a✝ l✝
⊢ ∀ (a : α), a ∈ l✝ → p a

Proof state:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h :
  match l with
  | [] => True
  | a :: l => Chain r a l
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : ∀ (lne : l ≠ []), p (l.head lne)
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
split at h

Result:
case h_1
α : Type u
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
x✝ : List α
initial : ∀ (lne : [] ≠ []), p ([].head lne)
h : True
⊢ ∀ (i : α), i ∈ [] → p i

case h_2
α : Type u
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
x✝ : List α
a✝ : α
l✝ : List α
initial : ∀ (lne : a✝ :: l✝ ≠ []), p ((a✝ :: l✝).head lne)
h : Chain r a✝ l✝
⊢ ∀ (i : α), i ∈ a✝ :: l✝ → p i

Proof state:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h : Chain' r l
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : ∀ (lne : l ≠ []), p (l.head lne)
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
unfold Chain' at h

Result:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h :
  match l with
  | [] => True
  | a :: l => Chain r a l
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : ∀ (lne : l ≠ []), p (l.head lne)
⊢ ∀ (i : α), i ∈ l → p i

Proof state:
case h_1
α : Type u
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
x✝ : List α
initial : ∀ (lne : [] ≠ []), p ([].head lne)
h : True
⊢ ∀ (i : α), i ∈ [] → p i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_then_self {p q : Prop} [h : Decidable p] : (if p then p else q) ↔ (¬p → q)

Proof state:
case isTrue
p q : Prop
h✝ : p
⊢ (if p then p else q) ↔ ¬p → q

Tactic:
rename_i g

Result:
case isTrue
p q : Prop
g : p
⊢ (if p then p else q) ↔ ¬p → q

Proof state:
p q : Prop
h : Decidable p
⊢ (if p then p else q) ↔ ¬p → q

Tactic:
cases h <;> (rename_i g; simp [g])

Result:
no goals

Proof state:
case isTrue
p q : Prop
g : p
⊢ (if p then p else q) ↔ ¬p → q

Tactic:
simp [g]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
lemma monovary_iff_forall_smul_nonneg : Monovary f g ↔ ∀ i j, 0 ≤ (f j - f i) • (g j - g i) :=
  monovaryOn_univ.symm.trans <| monovaryOn_iff_forall_smul_nonneg.trans <| by
    simp only [Set.mem_univ, forall_true_left]

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
⊢ (∀ ⦃i : ι⦄, i ∈ Set.univ → ∀ ⦃j : ι⦄, j ∈ Set.univ → 0 ≤ (f j - f i) • (g j - g i)) ↔
    ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)

Tactic:
simp only [Set.mem_univ, forall_true_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem getLast?_filterMap (f : α → Option β) (l : List α) : (l.filterMap f).getLast? = l.reverse.findSome? f

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ (filterMap f l).getLast? = findSome? f l.reverse

Tactic:
rw [getLast?_eq_head?_reverse]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ (filterMap f l).reverse.head? = findSome? f l.reverse

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ (filterMap f l).reverse.head? = findSome? f l.reverse

Tactic:
simp [← filterMap_reverse]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_zsmul_sub_toIcoMod (a b : α) : toIcoDiv hp a b • p + toIcoMod hp a b = b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b • p + toIcoMod hp a b = b

Tactic:
rw [add_comm, toIcoMod_add_toIcoDiv_zsmul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_eq_zipIdx_map {l : List α} {f : Nat → α → β} :
    l.mapIdx f = l.zipIdx.map (fun ⟨a, i⟩ => f i a)

Proof state:
case h
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
⊢ (mapIdx f l)[i]? =
    (map
        (fun x =>
          match x with
          | (a, i) => f i a)
        l.zipIdx)[i]?

Tactic:
simp only [getElem?_mapIdx, Option.map, getElem?_map, getElem?_zipIdx]

Result:
case h
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
⊢ (match l[i]? with
    | some x => some (f i x)
    | none => none) =
    match
      match l[i]? with
      | some x => some (x, 0 + i)
      | none => none with
    | some x => some (f x.snd x.fst)
    | none => none

Proof state:
case h
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
⊢ (match l[i]? with
    | some x => some (f i x)
    | none => none) =
    match
      match l[i]? with
      | some x => some (x, 0 + i)
      | none => none with
    | some x => some (f x.snd x.fst)
    | none => none

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
⊢ mapIdx f l =
    map
      (fun x =>
        match x with
        | (a, i) => f i a)
      l.zipIdx

Tactic:
ext1 i

Result:
case h
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
⊢ (mapIdx f l)[i]? =
    (map
        (fun x =>
          match x with
          | (a, i) => f i a)
        l.zipIdx)[i]?
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem powersEquivPowers_apply (h : orderOf x = orderOf y) (n : ℕ) :
    powersEquivPowers h ⟨x ^ n, n, rfl⟩ = ⟨y ^ n, n, rfl⟩

Proof state:
G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x y : G
h : orderOf x = orderOf y
n : ℕ
⊢ (finCongr h) ⟨n % orderOf x, ⋯⟩ = ⟨n % orderOf y, ⋯⟩

Tactic:
simp [h]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x y : G
h : orderOf x = orderOf y
n : ℕ
⊢ (powersEquivPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩

Tactic:
rw [powersEquivPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivPowers_symm_apply, ←
  Equiv.eq_symm_apply, finEquivPowers_symm_apply]

Result:
G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x y : G
h : orderOf x = orderOf y
n : ℕ
⊢ (finCongr h) ⟨n % orderOf x, ⋯⟩ = ⟨n % orderOf y, ⋯⟩
-- Mathlib/Data/Finset/Slice.lean
theorem _root_.Set.Sized.card_le (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
    #𝒜 ≤ (Fintype.card α).choose r

Proof state:
α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ #𝒜 ≤ #(powersetCard r univ)

Tactic:
exact card_le_card (subset_powersetCard_univ_iff.mpr h𝒜)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ #𝒜 ≤ (Fintype.card α).choose r

Tactic:
rw [Fintype.card, ← card_powersetCard]

Result:
α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ #𝒜 ≤ #(powersetCard r univ)
-- Mathlib/RingTheory/Prime.lean
theorem Prime.neg {p : α} (hp : Prime p) : Prime (-p)

Proof state:
case intro.intro
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ Prime (-p)

Tactic:
exact ⟨neg_ne_zero.mpr h1, by rwa [IsUnit.neg_iff], by simpa [neg_dvd] using h3⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ ∀ (a b : α), -p ∣ a * b → -p ∣ a ∨ -p ∣ b

Tactic:
simpa [neg_dvd] using h3

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ ¬IsUnit (-p)

Tactic:
rwa [IsUnit.neg_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommRing α
p : α
hp : Prime p
⊢ Prime (-p)

Tactic:
obtain ⟨h1, h2, h3⟩ := hp

Result:
case intro.intro
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ Prime (-p)
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_hom_ne_zero {s : Multiset α} (hs : s ≠ 0) {F : Type*} [FunLike F α β]
    [MulHomClass F α β] (f : F) :
    (s.map f).prod = f s.prod

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
F : Type u_7
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
a✝ : List α
hs : Quot.mk (⇑(List.isSetoid α)) a✝ ≠ 0
⊢ (map (⇑f) (Quot.mk (⇑(List.isSetoid α)) a✝)).prod = f (prod (Quot.mk (⇑(List.isSetoid α)) a✝))

Tactic:
aesop (add simp List.prod_hom_nonempty)

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Multiset α
hs : s ≠ 0
F : Type u_7
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
⊢ (map (⇑f) s).prod = f s.prod

Tactic:
induction s using Quot.inductionOn

Result:
case h
α : Type u_3
β : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
F : Type u_7
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
a✝ : List α
hs : Quot.mk (⇑(List.isSetoid α)) a✝ ≠ 0
⊢ (map (⇑f) (Quot.mk (⇑(List.isSetoid α)) a✝)).prod = f (prod (Quot.mk (⇑(List.isSetoid α)) a✝))
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_map_eq {β : Type u} {f : α → β} {X : Set β} (M : Matroid α) (hf : InjOn f M.E) :
    (M.map f hf).cRk X = M.cRk (f ⁻¹' X)

Proof state:
α β : Type u
f : α → β
X : Set β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf).cRk X = M.cRk (f ⁻¹' X)

Tactic:
rw [← M.cRk_inter_ground, ← M.cRk_map_image hf _, image_preimage_inter, ← map_ground _ _ hf,
  cRk_inter_ground]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem norm_iteratedFDeriv_fderiv {n : ℕ} :
    ‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ ‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖

Tactic:
rw [iteratedFDeriv_succ_eq_comp_right, comp_apply, LinearIsometryEquiv.norm_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
    {k a : α} {v : β} {h} : getValue a (insertEntry k v l) h =
      if h' : k == a then v
      else getValue a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h'))

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (insertEntry k v l) = true
⊢ getValue a (insertEntry k v l) h = if h' : (k == a) = true then v else getValue a l ⋯

Tactic:
rw [← Option.some_inj, ← getValue?_eq_some_getValue, apply_dite Option.some,
  getValue?_insertEntry, ← dite_eq_ite]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (insertEntry k v l) = true
⊢ (if x : (k == a) = true then some v else getValue? a l) =
    if h : (k == a) = true then some v else some (getValue a l ⋯)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (insertEntry k v l) = true
⊢ (if x : (k == a) = true then some v else getValue? a l) =
    if h : (k == a) = true then some v else some (getValue a l ⋯)

Tactic:
simp only [← getValue?_eq_some_getValue]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem bounded_le_inter_lt [LinearOrder α] (a : α) :
    Bounded (· ≤ ·) (s ∩ { b | a < b }) ↔ Bounded (· ≤ ·) s

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a < b}) ↔ Bounded (fun x1 x2 => x1 ≤ x2) s

Tactic:
simp_rw [← not_le, bounded_le_inter_not_le]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem mul_def (I J : FractionalIdeal S P) :
    I * J = ⟨I * J, I.isFractional.mul J.isFractional⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
⊢ I * J = ⟨↑I * ↑J, ⋯⟩

Tactic:
simp only [← mul_eq_mul, mul_def']

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem coe_sum {ι : Type*} [Fintype ι] (f : ι → S) : (↑(∑ i, f i) : L) = ∑ i, (f i : L)

Proof state:
case empty
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → ↥S
⊢ ↑(∑ i ∈ ∅, f i) = ∑ i ∈ ∅, ↑(f i)

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → ↥S
⊢ ↑(∑ i : ι, f i) = ∑ i : ι, ↑(f i)

Tactic:
induction' (Finset.univ : Finset ι) using Finset.induction_on with i s hi H

Result:
case empty
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → ↥S
⊢ ↑(∑ i ∈ ∅, f i) = ∑ i ∈ ∅, ↑(f i)

case insert
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → ↥S
i : ι
s : Finset ι
hi : i ∉ s
H : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
⊢ ↑(∑ i ∈ insert i s, f i) = ∑ i ∈ insert i s, ↑(f i)

Proof state:
case insert
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
S : IntermediateField K L
ι : Type u_4
inst✝ : Fintype ι
f : ι → ↥S
i : ι
s : Finset ι
hi : i ∉ s
H : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
⊢ ↑(∑ i ∈ insert i s, f i) = ∑ i ∈ insert i s, ↑(f i)

Tactic:
rw [Finset.sum_insert hi, AddMemClass.coe_add, H, Finset.sum_insert hi]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Outside the usual range of `binEntropy`, it is negative. This is due to `log p = log |p|`. -/
lemma binEntropy_nonpos_of_nonpos (hp : p ≤ 0) : binEntropy p ≤ 0

Proof state:
case inr
p : ℝ
hp✝ : p ≤ 0
hp : p < 0
⊢ binEntropy p ≤ 0

Tactic:
exact (binEntropy_neg_of_neg hp).le

Result:
no goals

Proof state:
p : ℝ
hp : p ≤ 0
⊢ binEntropy p ≤ 0

Tactic:
obtain rfl | hp := hp.eq_or_lt

Result:
case inl
hp : 0 ≤ 0
⊢ binEntropy 0 ≤ 0

case inr
p : ℝ
hp✝ : p ≤ 0
hp : p < 0
⊢ binEntropy p ≤ 0

Proof state:
case inl
hp : 0 ≤ 0
⊢ binEntropy 0 ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Array/ExtractLemmas.lean
theorem extract_eq_nil_of_start_eq_end {a : Array α} :
    a.extract i i = #[]

Proof state:
α : Type u
i : Nat
a : Array α
⊢ a.extract i i = #[]

Tactic:
refine extract_empty_of_stop_le_start a ?h

Result:
case h
α : Type u
i : Nat
a : Array α
⊢ i ≤ i

Proof state:
case h
α : Type u
i : Nat
a : Array α
⊢ i ≤ i

Tactic:
exact Nat.le_refl i

Result:
no goals
-- Mathlib/Algebra/Group/Idempotent.lean
lemma pow_succ_eq (n : ℕ) (h : IsIdempotentElem a) : a ^ (n + 1) = a :=
  Nat.recOn n ((Nat.zero_add 1).symm ▸ pow_one a) fun n ih => by rw [pow_succ, ih, h.eq]

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
⊢ a ^ (n.succ + 1) = a

Tactic:
rw [pow_succ, ih, h.eq]

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_sup {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} :
    Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y

Proof state:
α : Type u_1
β : Type u_2
f : α → β
x₁ x₂ : Filter α
y : Filter β
⊢ Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y

Tactic:
simp only [Tendsto, map_sup, sup_le_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_replaceEntry_of_containsKey_eq_false [BEq α] {l : List ((_ : α) × β)} {k a : α}
    {v : β} (hl : containsKey k l = false) : getValue? a (replaceEntry k v l) = getValue? a l

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
hl : containsKey k l = false
⊢ getValue? a (replaceEntry k v l) = getValue? a l

Tactic:
simp [getValue?_eq_getEntry?, getEntry?_replaceEntry_of_containsKey_eq_false hl]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
theorem ofAdd_image_zmultiples_eq_zpowers_ofAdd {x : A} :
    Multiplicative.ofAdd '' (AddSubgroup.zmultiples x : Set A) =
      Subgroup.zpowers (Multiplicative.ofAdd x)

Proof state:
A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x)

Tactic:
rw [Equiv.eq_image_iff_symm_image_eq]

Result:
A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ⇑Multiplicative.ofAdd.symm '' ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ↑(AddSubgroup.zmultiples x)

Proof state:
A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ⇑Multiplicative.ofAdd.symm '' ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ↑(AddSubgroup.zmultiples x)

Tactic:
exact ofMul_image_zpowers_eq_zmultiples_ofMul

Result:
no goals

Proof state:
A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (Multiplicative.ofAdd x))

Tactic:
symm

Result:
A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x)
-- Mathlib/Algebra/Module/Submodule/EqLocus.lean
theorem eqOn_sup {f g : F} {S T : Submodule R M} (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) :
    Set.EqOn f g ↑(S ⊔ T)

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : Set.EqOn ⇑f ⇑g ↑S
hT : Set.EqOn ⇑f ⇑g ↑T
⊢ Set.EqOn ⇑f ⇑g ↑(S ⊔ T)

Tactic:
rw [← le_eqLocus] at hS hT ⊢

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : S ≤ eqLocus f g
hT : T ≤ eqLocus f g
⊢ S ⊔ T ≤ eqLocus f g

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : S ≤ eqLocus f g
hT : T ≤ eqLocus f g
⊢ S ⊔ T ≤ eqLocus f g

Tactic:
exact sup_le hS hT

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_const (μ : Measure α) [IsFiniteMeasure μ] [h : NeZero μ] (c : ℝ≥0∞) :
    ⨍⁻ _x, c ∂μ = c

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
h : NeZero μ
c : ℝ≥0∞
⊢ ⨍⁻ (_x : α), c ∂μ = c

Tactic:
simp only [laverage, lintegral_const, measure_univ, mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem finrank_eq_one_iff' [Module.Free K V] :
    finrank K V = 1 ↔ ∃ v ≠ 0, ∀ w : V, ∃ c : K, c • v = w

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ finrank K V = 1 ↔ Module.rank K V = 1

Tactic:
exact toNat_eq_iff one_ne_zero

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ finrank K V = 1 ↔ ∃ v, v ≠ 0 ∧ ∀ (w : V), ∃ c, c • v = w

Tactic:
rw [← rank_eq_one_iff]

Result:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ finrank K V = 1 ↔ Module.rank K V = 1
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem basisRepr_apply [Fintype ι] {v : Basis ι R M} (Q : QuadraticMap R M N) (w : ι → R) :
    Q.basisRepr v w = Q (∑ i : ι, w i • v i)

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_8
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticMap R M N
w : ι → R
⊢ (Q.basisRepr v) w = Q (v.equivFun.symm w)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_8
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticMap R M N
w : ι → R
⊢ (Q.basisRepr v) w = Q (∑ i : ι, w i • v i)

Tactic:
rw [← v.equivFun_symm_apply]

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_8
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticMap R M N
w : ι → R
⊢ (Q.basisRepr v) w = Q (v.equivFun.symm w)
-- Mathlib/Algebra/Module/SpanRank.lean
theorem FG.exists_span_set_encard_eq_spanFinrank {p : Submodule R M} (h : p.FG) :
    ∃ s : Set M, s.encard = p.spanFinrank ∧ span R s = p

Proof state:
case intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
⊢ s.encard = ↑p.spanFinrank

Tactic:
have := fg_iff_spanRank_eq_spanFinrank.mpr h

Result:
case intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ s.encard = ↑p.spanFinrank

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
⊢ ∃ s, s.encard = ↑p.spanFinrank ∧ span R s = p

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p

Result:
case intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
⊢ ∃ s, s.encard = ↑p.spanFinrank ∧ span R s = p

Proof state:
case intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ s.encard = ↑p.spanFinrank

Tactic:
rw [Set.encard, ENat.card, spanFinrank, hs₁, this]

Result:
case intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ toENat ↑p.spanFinrank = ↑(toNat ↑p.spanFinrank)

Proof state:
case intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ toENat ↑p.spanFinrank = ↑(toNat ↑p.spanFinrank)

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
⊢ ∃ s, s.encard = ↑p.spanFinrank ∧ span R s = p

Tactic:
refine ⟨s, ⟨?_, hs₂⟩⟩

Result:
case intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
⊢ s.encard = ↑p.spanFinrank