harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem pseudoApply_aux {P Q : C} (f : P ⟶ Q) (a b : Over P) : a ≈ b → app f a ≈ app f b :=
  fun ⟨R, p, q, ep, Eq, comm⟩ =>
  ⟨R, p, q, ep, Eq, show p ≫ a.hom ≫ f = q ≫ b.hom ≫ f by rw [reassoc_of% comm]⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
a b : Over P
x✝ : a ≈ b
R : C
p : R ⟶ a.left
q : R ⟶ b.left
ep : Epi p
Eq : Epi q
comm : p ≫ a.hom = q ≫ b.hom
⊢ p ≫ a.hom ≫ f = q ≫ b.hom ≫ f

Tactic:
rw [reassoc_of% comm]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_subtype_perm [DecidableEq α] {s : Finset α} (f : Perm α) (h) :
    (f.subtypePerm h : Perm s).support = ({x | f x ≠ x} : Finset s)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s ↔ f x ∈ s
⊢ (f.subtypePerm h).support = filter (fun x => f ↑x ≠ ↑x) univ

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s ↔ f x ∈ s
a✝ : { x // x ∈ s }
⊢ a✝ ∈ (f.subtypePerm h).support ↔ a✝ ∈ filter (fun x => f ↑x ≠ ↑x) univ

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s ↔ f x ∈ s
a✝ : { x // x ∈ s }
⊢ a✝ ∈ (f.subtypePerm h).support ↔ a✝ ∈ filter (fun x => f ↑x ≠ ↑x) univ

Tactic:
simp [Subtype.ext_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem splitInTwo_fst_le_splitInTwo_snd {l : { l : List α // l.length = n }} (h : Pairwise le l.1) :
    ∀ a b, a ∈ (splitInTwo l).1.1 → b ∈ (splitInTwo l).2.1 → le a b

Proof state:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
a b : α
ma : a ∈ ⟨take ((n + 1) / 2) l.val, ⋯⟩.val
mb : b ∈ ⟨drop ((n + 1) / 2) l.val, ⋯⟩.val
⊢ le a b

Tactic:
exact h.rel_of_mem_take_of_mem_drop ma mb

Result:
no goals

Proof state:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
⊢ ∀ (a b : α), a ∈ ⟨take ((n + 1) / 2) l.val, ⋯⟩.val → b ∈ ⟨drop ((n + 1) / 2) l.val, ⋯⟩.val → le a b

Tactic:
intro a b ma mb

Result:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
a b : α
ma : a ∈ ⟨take ((n + 1) / 2) l.val, ⋯⟩.val
mb : b ∈ ⟨drop ((n + 1) / 2) l.val, ⋯⟩.val
⊢ le a b

Proof state:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
⊢ ∀ (a b : α), a ∈ (splitInTwo l).fst.val → b ∈ (splitInTwo l).snd.val → le a b

Tactic:
rw [splitInTwo_fst, splitInTwo_snd]

Result:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
⊢ ∀ (a b : α), a ∈ ⟨take ((n + 1) / 2) l.val, ⋯⟩.val → b ∈ ⟨drop ((n + 1) / 2) l.val, ⋯⟩.val → le a b
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_subset_Icc (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Icc a₁ b₁ ⊆ Icc a₂ b₂

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂

Tactic:
simpa [← coe_subset] using Set.Icc_subset_Icc ha hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_uShiftRight {x : BitVec w} {n : Nat} :
    (x >>> n).toFin = x.toFin / (Fin.ofNat' (2^w) (2^n))

Proof state:
case a
w : Nat
x : BitVec w
n : Nat
⊢ ↑(x >>> n).toFin = ↑(x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n))

Tactic:
by_cases hn : n < w

Result:
case pos
w : Nat
x : BitVec w
n : Nat
hn : n < w
⊢ ↑(x >>> n).toFin = ↑(x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n))

case neg
w : Nat
x : BitVec w
n : Nat
hn : ¬n < w
⊢ ↑(x >>> n).toFin = ↑(x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n))

Proof state:
case neg
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
⊢ ↑(x >>> n).toFin = ↑(x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n))

Tactic:
rw [ushiftRight_eq_zero (by omega)]

Result:
case neg
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
⊢ ↑(0#w).toFin = ↑(x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n))

Proof state:
case pos
w : Nat
x : BitVec w
n : Nat
hn : n < w
⊢ ↑(x >>> n).toFin = ↑(x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n))

Tactic:
simp [Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt (Nat.pow_lt_pow_of_lt Nat.one_lt_two hn)]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
⊢ (x >>> n).toFin = x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n)

Tactic:
apply Fin.eq_of_val_eq

Result:
case a
w : Nat
x : BitVec w
n : Nat
⊢ ↑(x >>> n).toFin = ↑(x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n))

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
⊢ w ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
n : Nat
hn : ¬n < w
⊢ ↑(x >>> n).toFin = ↑(x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n))

Tactic:
simp only [Nat.not_lt] at hn

Result:
case neg
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
⊢ ↑(x >>> n).toFin = ↑(x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n))

Proof state:
case neg
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
⊢ ↑(0#w).toFin = ↑(x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n))

Tactic:
simp [Nat.dvd_iff_mod_eq_zero.mp (Nat.pow_dvd_pow 2 hn)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_append_of_not_contains_right [BEq α] {l l' : List ((a : α) × β a)} {a : α}
    (hl' : containsKey a l' = false) : containsKey a (l ++ l') = containsKey a l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
a : α
hl' : containsKey a l' = false
⊢ containsKey a (l ++ l') = containsKey a l

Tactic:
simp [hl']

Result:
no goals
-- Mathlib/Algebra/BigOperators/NatAntidiagonal.lean
theorem prod_antidiagonal_succ' {n : ℕ} {f : ℕ × ℕ → M} : (∏ p ∈ antidiagonal (n + 1), f p) =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Tactic:
rw [← prod_antidiagonal_swap, prod_antidiagonal_succ, ← prod_antidiagonal_swap]

Result:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1).swap * ∏ p ∈ antidiagonal n, f (p.swap.1 + 1, p.swap.2).swap =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1).swap * ∏ p ∈ antidiagonal n, f (p.swap.1 + 1, p.swap.2).swap =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem bot_quotient_isMaximal_iff (I : Ideal R) [I.IsTwoSided] :
    (⊥ : Ideal (R ⧸ I)).IsMaximal ↔ I.IsMaximal :=
  ⟨fun hI =>
    mk_ker (I := I) ▸
      comap_isMaximal_of_surjective (Quotient.mk I) Quotient.mk_surjective (K := ⊥) (H := hI),
    fun hI => by
    letI := Quotient.divisionRing I
    exact bot_isMaximal⟩

Proof state:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
this : DivisionRing (R ⧸ I) := Quotient.divisionRing I
⊢ ⊥.IsMaximal

Tactic:
exact bot_isMaximal

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
⊢ ⊥.IsMaximal

Tactic:
letI := Quotient.divisionRing I

Result:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
this : DivisionRing (R ⧸ I) := Quotient.divisionRing I
⊢ ⊥.IsMaximal
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.countP_toArray (l : List α) : countP p l.toArray = l.countP p

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ countP p l.toArray = List.countP p l

Tactic:
simp [countP]

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ List.foldr (fun a acc => bif p a then acc + 1 else acc) 0 l = List.countP p l

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ List.foldr (fun a acc => bif p a then acc + 1 else acc) 0 [] = List.countP p []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : List.foldr (fun a acc => bif p a then acc + 1 else acc) 0 tail = List.countP p tail
⊢ List.foldr (fun a acc => bif p a then acc + 1 else acc) 0 (head :: tail) = List.countP p (head :: tail)

Tactic:
simp only [List.foldr_cons, ih, List.countP_cons]

Result:
case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : List.foldr (fun a acc => bif p a then acc + 1 else acc) 0 tail = List.countP p tail
⊢ (bif p head then List.countP p tail + 1 else List.countP p tail) = List.countP p tail + if p head = true then 1 else 0

Proof state:
case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : List.foldr (fun a acc => bif p a then acc + 1 else acc) 0 tail = List.countP p tail
⊢ (bif p head then List.countP p tail + 1 else List.countP p tail) = List.countP p tail + if p head = true then 1 else 0

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ List.foldr (fun a acc => bif p a then acc + 1 else acc) 0 l = List.countP p l

Tactic:
induction l with
| nil => rfl
| cons head tail ih =>
  simp only [List.foldr_cons, ih, List.countP_cons]
  split <;> simp_all

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem mul_same (i : l) (j : m) (k : n) (d : α) :
    stdBasisMatrix i j c * stdBasisMatrix j k d = stdBasisMatrix i k (c * d)

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
⊢ ∑ j_1 : m,
      of (fun i' j' => if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' => if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' => if i = i' ∧ k = j' then c * d else 0) a b

Tactic:
by_cases h₁ : i = a <;> by_cases h₂ : k = b <;> simp [h₁, h₂]

Result:
no goals

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
⊢ (stdBasisMatrix i j c * stdBasisMatrix j k d) a b = stdBasisMatrix i k (c * d) a b

Tactic:
simp only [mul_apply, stdBasisMatrix, boole_mul]

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
⊢ ∑ j_1 : m,
      of (fun i' j' => if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' => if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' => if i = i' ∧ k = j' then c * d else 0) a b

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
⊢ stdBasisMatrix i j c * stdBasisMatrix j k d = stdBasisMatrix i k (c * d)

Tactic:
ext a b

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
⊢ (stdBasisMatrix i j c * stdBasisMatrix j k d) a b = stdBasisMatrix i k (c * d) a b
-- Mathlib/CategoryTheory/Generator/Abelian.lean
theorem has_projective_separator [HasColimits C] [EnoughProjectives C] (G : C)
    (hG : IsCoseparator G) : ∃ G : C, Projective G ∧ IsSeparator G

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasColimits C
inst✝ : EnoughProjectives C
G : C
hG : IsCoseparator G
T : Cᵒᵖ
hT₁ : Injective T
hT₂ : IsCoseparator T
⊢ ∃ G, Projective G ∧ IsSeparator G

Tactic:
exact ⟨unop T, inferInstance, (isSeparator_unop_iff _).2 hT₂⟩

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasColimits C
inst✝ : EnoughProjectives C
G : C
hG : IsCoseparator G
⊢ ∃ G, Projective G ∧ IsSeparator G

Tactic:
obtain ⟨T, hT₁, hT₂⟩ := has_injective_coseparator (op G) ((isSeparator_op_iff _).2 hG)

Result:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasColimits C
inst✝ : EnoughProjectives C
G : C
hG : IsCoseparator G
T : Cᵒᵖ
hT₁ : Injective T
hT₂ : IsCoseparator T
⊢ ∃ G, Projective G ∧ IsSeparator G
-- Mathlib/Data/Fintype/Powerset.lean
lemma filter_subset_univ [DecidableEq α] (s : Finset α) :
    ({t | t ⊆ s} : Finset _) = powerset s

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun t => t ⊆ s) univ = s.powerset

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s a✝ : Finset α
⊢ a✝ ∈ filter (fun t => t ⊆ s) univ ↔ a✝ ∈ s.powerset

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s a✝ : Finset α
⊢ a✝ ∈ filter (fun t => t ⊆ s) univ ↔ a✝ ∈ s.powerset

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
protected lemma Frequently.uncurry {la : Filter α} {lb : Filter β} {p : α → β → Prop}
    (h : ∃ᶠ x in la, ∃ᶠ y in lb, p x y) : ∃ᶠ xy in la ×ˢ lb, p xy.1 xy.2 :=
  mt (fun h ↦ by simpa only [not_frequently] using h.curry) h

Proof state:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α → β → Prop
h✝ : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p x y
h : ∀ᶠ (x : α × β) in la ×ˢ lb, ¬(fun xy => p xy.1 xy.2) x
⊢ ∀ᶠ (x : α) in la, ¬(fun x => ∃ᶠ (y : β) in lb, p x y) x

Tactic:
simpa only [not_frequently] using h.curry

Result:
no goals
-- Mathlib/Order/Filter/CountableInter.lean
theorem eventually_countable_ball {ι : Type*} {S : Set ι} (hS : S.Countable)
    {p : α → ∀ i ∈ S, Prop} :
    (∀ᶠ x in l, ∀ i hi, p x i hi) ↔ ∀ i hi, ∀ᶠ x in l, p x i hi

Proof state:
α : Type u_2
l : Filter α
inst✝ : CountableInterFilter l
ι : Type u_4
S : Set ι
hS : S.Countable
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

Tactic:
simpa only [Filter.Eventually, setOf_forall] using
  @countable_bInter_mem _ l _ _ _ hS fun i hi => { x | p x i hi }

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem modify_eq_modifyTR : @modify = @modifyTR

Proof state:
case h.h.h.h
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ modify f n l = modifyTR f n l

Tactic:
simp [modifyTR, modifyTR_go_eq]

Result:
no goals

Proof state:
⊢ @modify = @modifyTR

Tactic:
funext α f n l

Result:
case h.h.h.h
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ modify f n l = modifyTR f n l
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
/-- The operator norm of the second projection `E × F → F` is at most 1. (It is 0 if `F` is zero, so
the inequality cannot be improved without further assumptions.) -/
lemma norm_snd_le : ‖snd 𝕜 E F‖ ≤ 1 :=
  opNorm_le_bound _ zero_le_one (fun ⟨e, f⟩ ↦ by simpa only [one_mul] using le_max_right ‖e‖ ‖f‖)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
x✝ : E × F
e : E
f : F
⊢ ‖(snd 𝕜 E F) (e, f)‖ ≤ 1 * ‖(e, f)‖

Tactic:
simpa only [one_mul] using le_max_right ‖e‖ ‖f‖

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem reflection_singleton_apply (u v : E) :
    reflection (𝕜 ∙ u) v = 2 • (⟪u, v⟫ / ((‖u‖ : 𝕜) ^ 2)) • u - v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
⊢ (reflection (Submodule.span 𝕜 {u})) v = 2 • (⟪u, v⟫_𝕜 / ↑‖u‖ ^ 2) • u - v

Tactic:
rw [reflection_apply, orthogonalProjection_singleton, ofReal_pow]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesWithinAt.continuousWithinAt_insert
    (hf : HasFPowerSeriesWithinAt f p s x) :
    ContinuousWithinAt f (insert x s) x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
⊢ ContinuousWithinAt f (insert x s) x

Tactic:
rcases hf with ⟨r, hr⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ ContinuousWithinAt f (insert x s) x

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ ContinuousWithinAt f (insert x s) x

Tactic:
apply hr.continuousWithinAt_insert

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
theorem trim_measurableSet_eq (hm : m ≤ m0) (hs : @MeasurableSet α m s) : μ.trim hm s = μ s

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
⊢ (μ.trim hm) s = μ s

Tactic:
rw [Measure.trim, toMeasure_apply (ms := m) _ _ hs, Measure.coe_toOuterMeasure]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem Finset.nnnorm_prod_le {α : Type*} [NormedCommRing α] [NormOneClass α] (s : Finset ι)
    (f : ι → α) : ‖∏ i ∈ s, f i‖₊ ≤ ∏ i ∈ s, ‖f i‖₊ :=
  (s.norm_prod_le f).trans_eq <| by simp [NNReal.coe_prod]

Proof state:
ι : Type u_4
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ∏ i ∈ s, ‖f i‖ = (fun a => ↑a) (∏ i ∈ s, ‖f i‖₊)

Tactic:
simp [NNReal.coe_prod]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
lemma imp_sup_left (φ ψ : L.BoundedFormula α n) : φ ⟹[T] φ ⊔ ψ := fun M v xs => by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]
  exact Or.inl

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
exact Or.inl

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⟹ φ ⊔ ψ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
lemma toShortNFOfCharThree_a₂ : (W.variableChange W.toShortNFOfCharThree).a₂ = W.b₂

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ 1 ^ 2 * (W.a₂ - 2 * -W.a₁ * W.a₁ + 3 * 0 - (2 * -W.a₁) ^ 2) = W.a₁ ^ 2 + 4 * W.a₂

Tactic:
linear_combination (-W.a₂ - W.a₁ ^ 2) * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ (W.variableChange W.toShortNFOfCharThree).a₂ = W.b₂

Tactic:
simp_rw [toShortNFOfCharThree, toCharNeTwoNF, variableChange_a₂, inv_one, Units.val_one, b₂]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ 1 ^ 2 * (W.a₂ - 2 * -W.a₁ * W.a₁ + 3 * 0 - (2 * -W.a₁) ^ 2) = W.a₁ ^ 2 + 4 * W.a₂
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_mul_const_Ioc_of_neg (a b : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c)

Tactic:
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, h, inter_comm]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
/-- The nonnegative distance between a point and its orthogonal projection to a subspace equals
the distance to that subspace as given by `Metric.infNndist`. This is not a `simp` lemma since
the simplest form depends on the context (if any calculations are to be done with the distance,
the version with the orthogonal projection gives access to more lemmas about orthogonal
projections that may be useful). -/
lemma dist_orthogonalProjection_eq_infNndist (s : AffineSubspace ℝ P) [Nonempty s]
    [HasOrthogonalProjection s.direction] (p : P) :
    nndist p (orthogonalProjection s p) = Metric.infNndist p s

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ nndist p ↑((orthogonalProjection s) p) = Metric.infNndist p ↑s

Tactic:
rw [← NNReal.coe_inj]

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑(nndist p ↑((orthogonalProjection s) p)) = ↑(Metric.infNndist p ↑s)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑(nndist p ↑((orthogonalProjection s) p)) = ↑(Metric.infNndist p ↑s)

Tactic:
simp [dist_orthogonalProjection_eq_infDist]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem logMap_eq_logEmbedding (u : (𝓞 K)ˣ) :
    logMap (mixedEmbedding K u) = logEmbedding K (Additive.ofMul u)

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x✝ : { w // w ≠ w₀ }
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) x✝ = (logEmbedding K) (Additive.ofMul u) x✝

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) = (logEmbedding K) (Additive.ofMul u)

Tactic:
ext

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x✝ : { w // w ≠ w₀ }
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) x✝ = (logEmbedding K) (Additive.ofMul u) x✝
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_const' (c : ℝ) : mgf (fun _ => c) μ t = (μ Set.univ).toReal * exp (t * c)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t c : ℝ
⊢ mgf (fun x => c) μ t = (μ Set.univ).toReal * rexp (t * c)

Tactic:
simp only [mgf, integral_const, smul_eq_mul]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem mem_smul_span_iff {v : ι → ℝ} :
    v ∈ (n : ℝ)⁻¹ • L ↔ ∀ i, n * v i ∈ Set.range (algebraMap ℤ ℝ)

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
v : ι → ℝ
⊢ v ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) ↔ ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)

Tactic:
rw [ZSpan.smul _ (inv_ne_zero (NeZero.ne _)), Basis.mem_span_iff_repr_mem]

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
v : ι → ℝ
⊢ (∀ (i : ι), (((Pi.basisFun ℝ ι).isUnitSMul ⋯).repr v) i ∈ Set.range ⇑(algebraMap ℤ ℝ)) ↔
    ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
v : ι → ℝ
⊢ (∀ (i : ι), (((Pi.basisFun ℝ ι).isUnitSMul ⋯).repr v) i ∈ Set.range ⇑(algebraMap ℤ ℝ)) ↔
    ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)

Tactic:
simp_rw [Basis.repr_isUnitSMul, Pi.basisFun_repr, Units.smul_def, Units.val_inv_eq_inv_val,
  IsUnit.unit_spec, inv_inv, smul_eq_mul]

Result:
no goals
-- Mathlib/Data/Int/AbsoluteValue.lean
theorem AbsoluteValue.map_units_int_smul (abv : AbsoluteValue R S) (x : ℤˣ) (y : R) :
    abv (x • y) = abv y

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
x : ℤˣ
y : R
⊢ abv (x • y) = abv y

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp

Result:
no goals