harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem AddSubmonoid.closure_isSquare [AddMonoid R] [Mul R] :
    closure {x : R | IsSquare x} = sumSq R

Proof state:
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
⊢ closure {x | IsSquare x} = sumSq R

Tactic:
refine closure_eq_of_le (fun x hx ↦ IsSquare.isSumSq hx) (fun x hx ↦ ?_)

Result:
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x : R
hx : x ∈ sumSq R
⊢ x ∈ closure {x | IsSquare x}

Proof state:
case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x a s✝ : R
hs : IsSumSq s✝
ih : s✝ ∈ closure {x | IsSquare x}
⊢ a * a + s✝ ∈ closure {x | IsSquare x}

Tactic:
exact add_mem (subset_closure (IsSquare.mul_self a)) ih

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x : R
⊢ 0 ∈ closure {x | IsSquare x}

Tactic:
apply zero_mem

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x : R
hx : x ∈ sumSq R
⊢ x ∈ closure {x | IsSquare x}

Tactic:
induction hx with
| zero => apply zero_mem
| sq_add a hs ih => exact add_mem (subset_closure (IsSquare.mul_self a)) ih

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_update_of_lt (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin m)
    (x : α (castLE h i)) : take m h (update v (castLE h i) x) = update (take m h v) i x

Proof state:
case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
rw [h']

Result:
case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) i = update (take m h v) i x i

Proof state:
case neg
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
this : castLE h j ≠ castLE h i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
simp only [take, update_of_ne h', update_of_ne this]

Result:
no goals

Proof state:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ castLE h j ≠ castLE h i

Tactic:
simp [h']

Result:
no goals

Proof state:
case neg
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
have : castLE h j ≠ castLE h i := by simp [h']

Result:
case neg
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
this : castLE h j ≠ castLE h i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Proof state:
case h
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
by_cases h' : j = i

Result:
case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

case neg
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Proof state:
case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) i = update (take m h v) i x i

Tactic:
simp only [take, update_self]

Result:
no goals

Proof state:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
⊢ take m h (update v (castLE h i) x) = update (take m h v) i x

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j
-- Mathlib/Probability/Moments/Basic.lean
theorem IndepFun.mgf_add {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ)
    (hX : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ)
    (hY : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ) :
    mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ
hY : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
simp_rw [mgf, Pi.add_apply, mul_add, exp_add]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ
hY : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ
⊢ ∫ (x : Ω), rexp (t * X x) * rexp (t * Y x) ∂μ = (∫ (x : Ω), rexp (t * X x) ∂μ) * ∫ (x : Ω), rexp (t * Y x) ∂μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
hX : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ
hY : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ
⊢ ∫ (x : Ω), rexp (t * X x) * rexp (t * Y x) ∂μ = (∫ (x : Ω), rexp (t * X x) ∂μ) * ∫ (x : Ω), rexp (t * Y x) ∂μ

Tactic:
exact (h_indep.exp_mul t t).integral_mul hX hY

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem Products.isGood_nil {I} [LinearOrder I] :
    Products.isGood ({fun _ ↦ false} : Set (I → Bool)) Products.nil

Proof state:
I : Type u_1
inst✝ : LinearOrder I
h : eval {fun x => false} nil ∈ Submodule.span ℤ (eval {fun x => false} '' {m | m < nil})
⊢ False

Tactic:
simp [Products.eval, Products.nil] at h

Result:
no goals

Proof state:
I : Type u_1
inst✝ : LinearOrder I
⊢ isGood {fun x => false} nil

Tactic:
intro h

Result:
I : Type u_1
inst✝ : LinearOrder I
h : eval {fun x => false} nil ∈ Submodule.span ℤ (eval {fun x => false} '' {m | m < nil})
⊢ False
-- Mathlib/Data/Real/Archimedean.lean
theorem sInf_le_sSup (s : Set ℝ) (h₁ : BddBelow s) (h₂ : BddAbove s) : sInf s ≤ sSup s

Proof state:
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
⊢ sInf s ≤ sSup s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Result:
case inl
h₁ : BddBelow ∅
h₂ : BddAbove ∅
⊢ sInf ∅ ≤ sSup ∅

case inr
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : s.Nonempty
⊢ sInf s ≤ sSup s

Proof state:
case inl
h₁ : BddBelow ∅
h₂ : BddAbove ∅
⊢ sInf ∅ ≤ sSup ∅

Tactic:
rw [sInf_empty, sSup_empty]

Result:
no goals

Proof state:
case inr
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : s.Nonempty
⊢ sInf s ≤ sSup s

Tactic:
exact csInf_le_csSup h₁ h₂ hne

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem Nodup.product : Nodup s → Nodup t → Nodup (s ×ˢ t) :=
  Quotient.inductionOn₂ s t fun l₁ l₂ d₁ d₂ => by simp [List.Nodup.product d₁ d₂]

Proof state:
α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
l₁ : List α
l₂ : List β
d₁ : Nodup ⟦l₁⟧
d₂ : Nodup ⟦l₂⟧
⊢ (⟦l₁⟧ ×ˢ ⟦l₂⟧).Nodup

Tactic:
simp [List.Nodup.product d₁ d₂]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasStrictFDerivAt.mul (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
    HasStrictFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ HasStrictFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x

Tactic:
convert hc.mul' hd

Result:
case h.e'_12.h.e'_6
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ d x • c' = c'.smulRight (d x)

Proof state:
case h.e'_12.h.e'_6.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
z : E
⊢ (d x • c') z = (c'.smulRight (d x)) z

Tactic:
apply mul_comm

Result:
no goals

Proof state:
case h.e'_12.h.e'_6
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ d x • c' = c'.smulRight (d x)

Tactic:
ext z

Result:
case h.e'_12.h.e'_6.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
z : E
⊢ (d x • c') z = (c'.smulRight (d x)) z
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem modOf_apply_of_exists_add (x : k[G]) (g : G) (g' : G)
    (h : ∃ d, g' = g + d) : (x %ᵒᶠ g) g' = 0

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ∃ d, g' = g + d
⊢ ¬¬∃ g₂, g' = g + g₂

Tactic:
rwa [Classical.not_not]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ∃ d, g' = g + d
⊢ (x %ᵒᶠ g) g' = 0

Tactic:
exact Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ∃ d, g' = g + d
⊢ (x %ᵒᶠ g) g' = 0

Tactic:
classical exact Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem lf_iff_lt_or_fuzzy {x y : PGame} : x ⧏ y ↔ x < y ∨ x ‖ y

Proof state:
x y : PGame
⊢ ¬y ≤ x ↔ x ≤ y ∧ ¬y ≤ x ∨ ¬y ≤ x ∧ ¬x ≤ y

Tactic:
tauto

Result:
no goals

Proof state:
x y : PGame
⊢ x ⧏ y ↔ x < y ∨ x ‖ y

Tactic:
simp only [lt_iff_le_and_lf, Fuzzy, ← PGame.not_le]

Result:
x y : PGame
⊢ ¬y ≤ x ↔ x ≤ y ∧ ¬y ≤ x ∨ ¬y ≤ x ∧ ¬x ≤ y
-- Mathlib/Algebra/Order/Ring/WithTop.lean
theorem top_pow {n : ℕ} (n_pos : 0 < n) : (⊤ : WithTop α) ^ n = ⊤ :=
  Nat.le_induction (pow_one _) (fun m _ hm => by rw [pow_succ, hm, top_mul_top]) _
    (Nat.succ_le_of_lt n_pos)

Proof state:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
n_pos : 0 < n
m : ℕ
x✝ : Nat.succ 0 ≤ m
hm : ⊤ ^ m = ⊤
⊢ ⊤ ^ (m + 1) = ⊤

Tactic:
rw [pow_succ, hm, top_mul_top]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Basic.lean
lemma hom_inv_apply {M N : ModuleCat.{v} R} (e : M ≅ N) (x : N) : e.hom (e.inv x) = x

Proof state:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
e : M ≅ N
x : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Order/WellQuasiOrder.lean
theorem Finite.wellQuasiOrdered (r : α → α → Prop) [Finite α] [IsRefl α r] :
    WellQuasiOrdered r

Proof state:
α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : IsRefl α r
f : ℕ → α
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨m, n, h, hf⟩ := Set.finite_univ.exists_lt_map_eq_of_forall_mem (f := f)
  fun _ ↦ Set.mem_univ _

Result:
case intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : IsRefl α r
f : ℕ → α
m n : ℕ
h : m < n
hf : f m = f n
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : IsRefl α r
⊢ WellQuasiOrdered r

Tactic:
intro f

Result:
α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : IsRefl α r
f : ℕ → α
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Proof state:
case intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : IsRefl α r
f : ℕ → α
m n : ℕ
h : m < n
hf : f m = f n
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
exact ⟨m, n, h, hf ▸ refl _⟩

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_comm (a b : α) : a ⊔ b = b ⊔ a

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b = b ⊔ a

Tactic:
apply le_antisymm <;> simp

Result:
no goals
-- Mathlib/Order/WellFounded.lean
theorem WellFounded.self_le_of_strictMono (h : WellFounded ((· < ·) : β → β → Prop))
    {f : β → β} (hf : StrictMono f) : ∀ n, n ≤ f n

Proof state:
β : Type u_2
inst✝ : LinearOrder β
h : WellFounded fun x1 x2 => x1 < x2
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
h₂ : h.min (fun x => Preorder.toLT.1 (f x) x) h₁ ∈ fun x => Preorder.toLT.1 (f x) x
⊢ False

Tactic:
exact h.not_lt_min _ h₁ (hf h₂) h₂

Result:
no goals

Proof state:
β : Type u_2
inst✝ : LinearOrder β
h : WellFounded fun x1 x2 => x1 < x2
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
⊢ False

Tactic:
have h₂ := h.min_mem _ h₁

Result:
β : Type u_2
inst✝ : LinearOrder β
h : WellFounded fun x1 x2 => x1 < x2
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
h₂ : h.min (fun x => Preorder.toLT.1 (f x) x) h₁ ∈ fun x => Preorder.toLT.1 (f x) x
⊢ False

Proof state:
β : Type u_2
inst✝ : LinearOrder β
h : WellFounded fun x1 x2 => x1 < x2
f : β → β
hf : StrictMono f
⊢ ∀ (n : β), n ≤ f n

Tactic:
by_contra! h₁

Result:
β : Type u_2
inst✝ : LinearOrder β
h : WellFounded fun x1 x2 => x1 < x2
f : β → β
hf : StrictMono f
h₁ : ∃ n, f n < n
⊢ False
-- Mathlib/Data/Finset/Slice.lean
theorem sized_iUnion {f : ι → Set (Finset α)} : (⋃ i, f i).Sized r ↔ ∀ i, (f i).Sized r

Proof state:
α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ (∀ ⦃x : Finset α⦄ (x_1 : ι), x ∈ f x_1 → #x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → #x = r

Tactic:
exact forall_swap

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ Sized r (⋃ i, f i) ↔ ∀ (i : ι), Sized r (f i)

Tactic:
simp_rw [Set.Sized, Set.mem_iUnion, forall_exists_index]

Result:
α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ (∀ ⦃x : Finset α⦄ (x_1 : ι), x ∈ f x_1 → #x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → #x = r
-- Mathlib/Data/Real/Hyperreal.lean
theorem gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : Tendsto f atTop (𝓝 0)) :
    ∀ {r : ℝ}, r < 0 → (r : ℝ*) < ofSeq f := fun {r} hr => by
  rw [← neg_neg r, coe_neg]; exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)

Proof state:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ -↑(-r) < ofSeq f

Tactic:
exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)

Result:
no goals

Proof state:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ ↑r < ofSeq f

Tactic:
rw [← neg_neg r, coe_neg]

Result:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ -↑(-r) < ofSeq f
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
@[simp] lemma iteratedFDerivComponent_apply {α : Type*} [Fintype α]
    (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ s) [DecidablePred (· ∈ s)]
    (v : ∀ i : {a : ι // a ∉ s}, E₁ i) (w : α → (∀ i, E₁ i)) :
    f.iteratedFDerivComponent e v w =
      f (fun j ↦ if h : j ∈ s then w (e.symm ⟨j, h⟩) j else v ⟨j, h⟩)

Proof state:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x => x ∈ s
v : (i : { a // a ∉ s }) → E₁ ↑i
w : α → (i : ι) → E₁ i
⊢ ((f.iteratedFDerivComponent e) v) w = f fun j => if h : j ∈ s then w (e.symm ⟨j, h⟩) j else v ⟨j, h⟩

Tactic:
simp [iteratedFDerivComponent, MultilinearMap.iteratedFDerivComponent,
  MultilinearMap.domDomRestrictₗ]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithTop.ofDual_lt_iff {x : WithTop αᵒᵈ} {y : WithBot α} :
    WithTop.ofDual x < y ↔ WithBot.toDual y < x

Proof state:
α : Type u_1
inst✝ : LT α
x : WithTop αᵒᵈ
y : WithBot α
⊢ WithTop.ofDual x < y ↔ WithBot.toDual y < x

Tactic:
cases x <;> cases y <;> simp [toDual_lt]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem card_compress (huv : #u = #v) (a : Finset α) : #(compress u v a) = #a

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : ¬(Disjoint u a ∧ v ≤ a)
⊢ #a = #a

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ≤ a
⊢ #((a ⊔ u) \ v) = #a

Tactic:
rw [card_sdiff (h.2.trans le_sup_left), sup_eq_union, card_union_of_disjoint h.1.symm, huv,
  add_tsub_cancel_right]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
⊢ #(if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = #a

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ≤ a
⊢ #((a ⊔ u) \ v) = #a

case neg
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : ¬(Disjoint u a ∧ v ≤ a)
⊢ #a = #a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
⊢ #(compress u v a) = #a

Tactic:
unfold compress

Result:
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
⊢ #(if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = #a
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_finset_sup' (p : ι → Seminorm 𝕜 E) (s : Finset ι) (H : s.Nonempty) (e : E)
    (r : ℝ) : closedBall (s.sup' H p) e r = s.inf' H fun i => closedBall (p i) e r

Proof state:
case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : (s✝.sup' hs p).closedBall e r = s✝.inf' hs fun i => (p i).closedBall e r
⊢ ((Finset.cons a✝ s✝ h✝).sup' ⋯ p).closedBall e r = (Finset.cons a✝ s✝ h✝).inf' ⋯ fun i => (p i).closedBall e r

Tactic:
rw [Finset.sup'_cons hs, Finset.inf'_cons hs, closedBall_sup]

Result:
case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : (s✝.sup' hs p).closedBall e r = s✝.inf' hs fun i => (p i).closedBall e r
⊢ (p a✝).closedBall e r ∩ (s✝.sup' hs p).closedBall e r =
    (p a✝).closedBall e r ⊓ s✝.inf' hs fun i => (p i).closedBall e r

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
H : s.Nonempty
e : E
r : ℝ
⊢ (s.sup' H p).closedBall e r = s.inf' H fun i => (p i).closedBall e r

Tactic:
induction H using Finset.Nonempty.cons_induction with
| singleton => simp
| cons _ _ _ hs ih =>
  rw [Finset.sup'_cons hs, Finset.inf'_cons hs, closedBall_sup]
  simp only [inf_eq_inter, ih]

Result:
no goals

Proof state:
case singleton
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
⊢ ({a✝}.sup' ⋯ p).closedBall e r = {a✝}.inf' ⋯ fun i => (p i).closedBall e r

Tactic:
simp

Result:
no goals

Proof state:
case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : (s✝.sup' hs p).closedBall e r = s✝.inf' hs fun i => (p i).closedBall e r
⊢ (p a✝).closedBall e r ∩ (s✝.sup' hs p).closedBall e r =
    (p a✝).closedBall e r ⊓ s✝.inf' hs fun i => (p i).closedBall e r

Tactic:
simp only [inf_eq_inter, ih]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_congr [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α}
    (h : a == b) : containsKey a l = containsKey b l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a b : α
h : (a == b) = true
⊢ containsKey a l = containsKey b l

Tactic:
simp [containsKey_eq_isSome_getEntry?, getEntry?_congr h]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem symm_trans_self (e : α ≃ β) : e.symm.trans e = Equiv.refl β := ext <| by simp

Proof state:
α : Sort u
β : Sort v
e : α ≃ β
⊢ ∀ (x : β), (e.symm.trans e) x = (Equiv.refl β) x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem one_sub_gold : 1 - ψ = φ

Proof state:
⊢ 1 - ψ = φ

Tactic:
linarith [gold_add_goldConj]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem _root_.Cardinal.natCast_eq_toENat_iff {n : ℕ} {c : Cardinal} :
    ↑n = toENat c ↔ ↑n = c

Proof state:
n : ℕ
c : Cardinal.{u_3}
⊢ ↑n = toENat c ↔ ↑n = c

Tactic:
rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toENat_le_natCast_iff,
  Cardinal.natCast_le_toENat_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem denote_mkXorCached {aig : AIG α} {input : BinaryInput aig} :
    ⟦aig.mkXorCached input, assign⟧
      =
    xor
      ⟦aig, input.lhs, assign⟧
      ⟦aig, input.rhs, assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkXorCached input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧)

Tactic:
rw [← xor_as_aig]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkXorCached input⟧ =
    (!(⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧) &&
      !(!⟦assign, { aig := aig, ref := input.lhs }⟧ && !⟦assign, { aig := aig, ref := input.rhs }⟧))

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkXorCached input⟧ =
    (!(⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧) &&
      !(!⟦assign, { aig := aig, ref := input.lhs }⟧ && !⟦assign, { aig := aig, ref := input.rhs }⟧))

Tactic:
simp [
  mkXorCached,
  LawfulOperator.denote_mem_prefix (f := mkGateCached) input.lhs.hgate,
  LawfulOperator.denote_mem_prefix (f := mkGateCached) input.rhs.hgate
]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_eq_integral [IsProbabilityMeasure μ] (f : α → E) : ⨍ x, f x ∂μ = ∫ x, f x ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → E
⊢ ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
rw [average, measure_univ, inv_one, one_smul]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem trans_refl (α : X ≅ Y) : α ≪≫ Iso.refl Y = α

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ α ≪≫ refl Y = α

Tactic:
ext

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (α ≪≫ refl Y).hom = α.hom

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (α ≪≫ refl Y).hom = α.hom

Tactic:
apply Category.comp_id

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_add_le [DecidableEq σ] {p q : MvPolynomial σ R} :
    (p + q).degrees ≤ p.degrees ⊔ q.degrees

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p + q).degrees ≤ p.degrees ⊔ q.degrees

Tactic:
simp_rw [degrees_def]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ ((p + q).support.sup fun s => toMultiset s) ≤
    (p.support.sup fun s => toMultiset s) ⊔ q.support.sup fun s => toMultiset s

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ ((p + q).support.sup fun s => toMultiset s) ≤
    (p.support.sup fun s => toMultiset s) ⊔ q.support.sup fun s => toMultiset s

Tactic:
exact supDegree_add_le

Result:
no goals