harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_conj_eq_ite (x : ℂ) : log (conj x) = if x.arg = π then log x else conj (log x)

Proof state:
x : ℂ
⊢ log ((starRingEnd ℂ) x) = if x.arg = π then log x else (starRingEnd ℂ) (log x)

Tactic:
simp_rw [log, norm_conj, arg_conj, map_add, map_mul, conj_ofReal]

Result:
x : ℂ
⊢ ↑(Real.log ‖x‖) + ↑(if x.arg = π then π else -x.arg) * I =
    if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I

Proof state:
case pos
x : ℂ
hx : x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑π * I = ↑(Real.log ‖x‖) + ↑x.arg * I

Tactic:
rw [hx]

Result:
no goals

Proof state:
case neg
x : ℂ
hx : ¬x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑(-x.arg) * I = ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I

Tactic:
simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]

Result:
no goals

Proof state:
x : ℂ
⊢ ↑(Real.log ‖x‖) + ↑(if x.arg = π then π else -x.arg) * I =
    if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I

Tactic:
split_ifs with hx

Result:
case pos
x : ℂ
hx : x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑π * I = ↑(Real.log ‖x‖) + ↑x.arg * I

case neg
x : ℂ
hx : ¬x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑(-x.arg) * I = ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem isDomain' {A B : Type*} [Field A] [Algebra F A] [Field B] [Algebra F B]
    {fa : A →ₐ[F] E} {fb : B →ₐ[F] E} (H : fa.fieldRange.LinearDisjoint fb.fieldRange) :
    IsDomain (A ⊗[F] B)

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Algebra F A
inst✝¹ : Field B
inst✝ : Algebra F B
fa : A →ₐ[F] E
fb : B →ₐ[F] E
H : fa.fieldRange.LinearDisjoint ↥fb.fieldRange
⊢ IsDomain (A ⊗[F] B)

Tactic:
simp_rw [linearDisjoint_iff', AlgHom.fieldRange_toSubalgebra] at H

Result:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Algebra F A
inst✝¹ : Field B
inst✝ : Algebra F B
fa : A →ₐ[F] E
fb : B →ₐ[F] E
H : fa.range.LinearDisjoint fb.range
⊢ IsDomain (A ⊗[F] B)

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Algebra F A
inst✝¹ : Field B
inst✝ : Algebra F B
fa : A →ₐ[F] E
fb : B →ₐ[F] E
H : fa.range.LinearDisjoint fb.range
⊢ IsDomain (A ⊗[F] B)

Tactic:
exact H.isDomain_of_injective fa.injective fb.injective

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get? i

Proof state:
α : Type u_1
a : Array α
i : Nat
⊢ a.get? i = a.toList.get? i

Tactic:
simp [← getElem?_toList]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem empty_append (as : Vector α n) : (#v[] : Vector α 0) ++ as = as.cast (by omega)

Proof state:
case mk
α : Type u_1
as : Array α
⊢ { toArray := #[], size_toArray := ⋯ } ++ { toArray := as, size_toArray := ⋯ } =
    Vector.cast ⋯ { toArray := as, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.216126
n : Nat
as : Vector α n
⊢ n = 0 + n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
as : Vector α n
⊢ { toArray := #[], size_toArray := ⋯ } ++ as = Vector.cast ⋯ as

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
as : Array α
⊢ { toArray := #[], size_toArray := ⋯ } ++ { toArray := as, size_toArray := ⋯ } =
    Vector.cast ⋯ { toArray := as, size_toArray := ⋯ }
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma neighborSet_eq_of_equiv {v : V} {H : Subgraph G}
    (h : G.neighborSet v ≃ H.neighborSet v) (hfin : (G.neighborSet v).Finite) :
    H.neighborSet v = G.neighborSet v

Proof state:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ↑(G.neighborSet v) ≃ ↑(H.neighborSet v)
hfin : (G.neighborSet v).Finite
⊢ H.neighborSet v = G.neighborSet v

Tactic:
lift H.neighborSet v to Finset V using h.set_finite_iff.mp hfin with s hs

Result:
case intro
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
hfin : (G.neighborSet v).Finite
s : Finset V
hs : ↑s = H.neighborSet v
h✝ h : ↑(G.neighborSet v) ≃ ↑↑s
⊢ ↑s = G.neighborSet v

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
h✝¹ : ↑(G.neighborSet v) ≃ ↑↑s
t : Finset V
ht : ↑t = G.neighborSet v
h✝ h : ↑↑t ≃ ↑↑s
⊢ ↑s = ↑t

Tactic:
refine congrArg _ <| Finset.eq_of_subset_of_card_le ?_ (Finset.card_eq_of_equiv h).le

Result:
case intro.intro
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
h✝¹ : ↑(G.neighborSet v) ≃ ↑↑s
t : Finset V
ht : ↑t = G.neighborSet v
h✝ h : ↑↑t ≃ ↑↑s
⊢ s ⊆ t

Proof state:
case intro
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
hfin : (G.neighborSet v).Finite
s : Finset V
hs : ↑s = H.neighborSet v
h✝ h : ↑(G.neighborSet v) ≃ ↑↑s
⊢ ↑s = G.neighborSet v

Tactic:
lift G.neighborSet v to Finset V using hfin with t ht

Result:
case intro.intro
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
h✝¹ : ↑(G.neighborSet v) ≃ ↑↑s
t : Finset V
ht : ↑t = G.neighborSet v
h✝ h : ↑↑t ≃ ↑↑s
⊢ ↑s = ↑t

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
h✝¹ : ↑(G.neighborSet v) ≃ ↑↑s
t : Finset V
ht : ↑t = G.neighborSet v
h✝ h : ↑↑t ≃ ↑↑s
⊢ s ⊆ t

Tactic:
rw [← Finset.coe_subset, hs, ht]

Result:
case intro.intro
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
h✝¹ : ↑(G.neighborSet v) ≃ ↑↑s
t : Finset V
ht : ↑t = G.neighborSet v
h✝ h : ↑↑t ≃ ↑↑s
⊢ H.neighborSet v ⊆ G.neighborSet v

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
h✝¹ : ↑(G.neighborSet v) ≃ ↑↑s
t : Finset V
ht : ↑t = G.neighborSet v
h✝ h : ↑↑t ≃ ↑↑s
⊢ H.neighborSet v ⊆ G.neighborSet v

Tactic:
exact H.neighborSet_subset _

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem reflection_orthogonal_vadd {s : AffineSubspace ℝ P} [Nonempty s]
    [HasOrthogonalProjection s.direction] {p : P} (hp : p ∈ s) {v : V} (hv : v ∈ s.directionᗮ) :
    reflection s (v +ᵥ p) = -v +ᵥ p

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
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ (↑⟨p, hp⟩ -ᵥ p - v) +ᵥ ↑⟨p, hp⟩ = -v +ᵥ p

Tactic:
simp

Result:
no goals

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
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ (reflection s) (v +ᵥ p) = -v +ᵥ p

Tactic:
rw [reflection_apply, orthogonalProjection_vadd_eq_self hp hv, vsub_vadd_eq_vsub_sub]

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
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ (↑⟨p, hp⟩ -ᵥ p - v) +ᵥ ↑⟨p, hp⟩ = -v +ᵥ p
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma map_comp {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂)
    (Φ : C ⥤ D) [Φ.Additive] :
    (Cochain.comp z₁ z₂ h).map Φ = Cochain.comp (z₁.map Φ) (z₂.map Φ) h

Proof state:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
F G K : CochainComplex C ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : C ⥤ D
inst✝ : Φ.Additive
p q : ℤ
hpq : p + n₁₂ = q
⊢ Φ.map ((z₁.comp z₂ h).v p q hpq) = ((z₁.map Φ).comp (z₂.map Φ) h).v p q hpq

Tactic:
simp only [map_v, comp_v _ _ h p _ q rfl (by omega), Φ.map_comp]

Result:
no goals

Proof state:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
F G K : CochainComplex C ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : C ⥤ D
inst✝ : Φ.Additive
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((z₁.comp z₂ h).map Φ).v p q hpq = ((z₁.map Φ).comp (z₂.map Φ) h).v p q hpq

Tactic:
dsimp

Result:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
F G K : CochainComplex C ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : C ⥤ D
inst✝ : Φ.Additive
p q : ℤ
hpq : p + n₁₂ = q
⊢ Φ.map ((z₁.comp z₂ h).v p q hpq) = ((z₁.map Φ).comp (z₂.map Φ) h).v p q hpq

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
F G K : CochainComplex C ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : C ⥤ D
inst✝ : Φ.Additive
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
F G K : CochainComplex C ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ (z₁.comp z₂ h).map Φ = (z₁.map Φ).comp (z₂.map Φ) h

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
F G K : CochainComplex C ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : C ⥤ D
inst✝ : Φ.Additive
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((z₁.comp z₂ h).map Φ).v p q hpq = ((z₁.map Φ).comp (z₂.map Φ) h).v p q hpq
-- Mathlib/Data/Fin/Basic.lean
lemma exists_succAbove_eq {x y : Fin (n + 1)} (h : x ≠ y) : ∃ z, y.succAbove z = x

Proof state:
case inl
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hxy : x < y
⊢ ∃ z, y.succAbove z = x

case inr
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hyx : y < x
⊢ ∃ z, y.succAbove z = x

Tactic:
exacts [⟨_, succAbove_castPred_of_lt _ _ hxy⟩, ⟨_, succAbove_pred_of_lt _ _ hyx⟩]

Result:
no goals

Proof state:
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
⊢ ∃ z, y.succAbove z = x

Tactic:
obtain hxy | hyx := Fin.lt_or_lt_of_ne h

Result:
case inl
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hxy : x < y
⊢ ∃ z, y.succAbove z = x

case inr
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hyx : y < x
⊢ ∃ z, y.succAbove z = x
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem HasLineDerivAt.of_comp {v : E'} (hf : HasLineDerivAt 𝕜 (f ∘ L) f' x v) :
    HasLineDerivAt 𝕜 f f' (L x) (L v)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type u_3
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
E' : Type u_4
inst✝¹ : AddCommGroup E'
inst✝ : Module 𝕜 E'
f : E → F
f' : F
x : E'
L : E' →ₗ[𝕜] E
v : E'
hf : HasLineDerivAt 𝕜 (f ∘ ⇑L) f' x v
⊢ HasLineDerivAt 𝕜 f f' (L x) (L v)

Tactic:
simpa [HasLineDerivAt] using hf

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem image_maximalIdeal : ((↑) : A → K) '' IsLocalRing.maximalIdeal A = A.nonunits

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ Subtype.val '' ↑(IsLocalRing.maximalIdeal ↥A) = ↑A.nonunits

Tactic:
ext a

Result:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : K
⊢ a ∈ Subtype.val '' ↑(IsLocalRing.maximalIdeal ↥A) ↔ a ∈ ↑A.nonunits

Proof state:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : K
⊢ a ∈ Subtype.val '' ↑(IsLocalRing.maximalIdeal ↥A) ↔ a ∈ ↑A.nonunits

Tactic:
simp only [Set.mem_image, SetLike.mem_coe, mem_nonunits_iff_exists_mem_maximalIdeal]

Result:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : K
⊢ (∃ x ∈ IsLocalRing.maximalIdeal ↥A, ↑x = a) ↔ ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ IsLocalRing.maximalIdeal ↥A

Proof state:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : K
⊢ (∃ x ∈ IsLocalRing.maximalIdeal ↥A, ↑x = a) ↔ ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ IsLocalRing.maximalIdeal ↥A

Tactic:
rw [Subtype.exists]

Result:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : K
⊢ (∃ a_1, ∃ (b : a_1 ∈ A), ⟨a_1, b⟩ ∈ IsLocalRing.maximalIdeal ↥A ∧ ↑⟨a_1, b⟩ = a) ↔
    ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ IsLocalRing.maximalIdeal ↥A

Proof state:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : K
⊢ (∃ a_1, ∃ (b : a_1 ∈ A), ⟨a_1, b⟩ ∈ IsLocalRing.maximalIdeal ↥A ∧ ↑⟨a_1, b⟩ = a) ↔
    ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ IsLocalRing.maximalIdeal ↥A

Tactic:
simp_rw [exists_and_right, exists_eq_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.mem_iff {a : α} {l₁ l₂ : List α} (p : l₁ ~ l₂) : a ∈ l₁ ↔ a ∈ l₂

Proof state:
α : Type u_1
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ a ∈ l₁ ↔ a ∈ l₂

Tactic:
induction p with
| nil => rfl
| cons _ _ ih => simp only [mem_cons, ih]
| swap => simp only [mem_cons, or_left_comm]
| trans _ _ ih₁ ih₂ => simp only [ih₁, ih₂]

Result:
no goals

Proof state:
case swap
α : Type u_1
a : α
l₁ l₂ : List α
x✝ y✝ : α
l✝ : List α
⊢ a ∈ y✝ :: x✝ :: l✝ ↔ a ∈ x✝ :: y✝ :: l✝

Tactic:
simp only [mem_cons, or_left_comm]

Result:
no goals

Proof state:
case trans
α : Type u_1
a : α
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : a ∈ l₁✝ ↔ a ∈ l₂✝
ih₂ : a ∈ l₂✝ ↔ a ∈ l₃✝
⊢ a ∈ l₁✝ ↔ a ∈ l₃✝

Tactic:
simp only [ih₁, ih₂]

Result:
no goals

Proof state:
case nil
α : Type u_1
a : α
l₁ l₂ : List α
⊢ a ∈ [] ↔ a ∈ []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
ih : a ∈ l₁✝ ↔ a ∈ l₂✝
⊢ a ∈ x✝ :: l₁✝ ↔ a ∈ x✝ :: l₂✝

Tactic:
simp only [mem_cons, ih]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem inf_sdiff_right (hs : s.Nonempty) (f : ι → α) (a : α) :
    (s.inf fun b => f b \ a) = s.inf f \ a

Proof state:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ ({a✝}.inf fun b => f b \ a) = {a✝}.inf f \ a

Tactic:
rw [inf_singleton, inf_singleton]

Result:
no goals

Proof state:
case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (s✝.inf fun b => f b \ a) = s✝.inf f \ a
⊢ ((cons a✝ s✝ h✝).inf fun b => f b \ a) = (cons a✝ s✝ h✝).inf f \ a

Tactic:
rw [inf_cons, inf_cons, ih, inf_sdiff]

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.inf fun b => f b \ a) = s.inf f \ a

Tactic:
induction hs using Finset.Nonempty.cons_induction with
| singleton => rw [inf_singleton, inf_singleton]
| cons _ _ _ _ ih => rw [inf_cons, inf_cons, ih, inf_sdiff]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Field.lean
theorem one_div_lt_one_div {n m : ℕ} (h : n < m) : 1 / ((m : α) + 1) < 1 / ((n : α) + 1)

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ 1 / (↑m + 1) < 1 / (↑n + 1)

Tactic:
refine one_div_lt_one_div_of_lt ?_ ?_

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ 0 < ↑n + 1

case refine_2
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ ↑n + 1 < ↑m + 1

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ 0 < ↑n + 1

Tactic:
exact Nat.cast_add_one_pos _

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrderedSemifield α
n m : ℕ
h : n < m
⊢ ↑n + 1 < ↑m + 1

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem leadingCoeff_comp (hq : natDegree q ≠ 0) :
    leadingCoeff (p.comp q) = leadingCoeff p * leadingCoeff q ^ natDegree p

Proof state:
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hq : q.natDegree ≠ 0
⊢ (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem nat_lt : PrimrecRel ((· < ·) : ℕ → ℕ → Prop) :=
  (nat_le.comp snd fst).not.of_eq fun p => by simp

Proof state:
p : ℕ × ℕ
⊢ ¬p.2 ≤ p.1 ↔ (fun x1 x2 => x1 < x2) p.1 p.2

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Derivation/Basic.lean
theorem map_aeval (P : R[X]) (x : A) :
    D (aeval x P) = aeval x (derivative P) • D x

Proof state:
case h_C
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
a✝ : R
⊢ D ((aeval x) (C a✝)) = (aeval x) (derivative (C a✝)) • D x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
P : R[X]
x : A
⊢ D ((aeval x) P) = (aeval x) (derivative P) • D x

Tactic:
induction P using Polynomial.induction_on

Result:
case h_C
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
a✝ : R
⊢ D ((aeval x) (C a✝)) = (aeval x) (derivative (C a✝)) • D x

case h_add
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
p✝ q✝ : R[X]
a✝¹ : D ((aeval x) p✝) = (aeval x) (derivative p✝) • D x
a✝ : D ((aeval x) q✝) = (aeval x) (derivative q✝) • D x
⊢ D ((aeval x) (p✝ + q✝)) = (aeval x) (derivative (p✝ + q✝)) • D x

case h_monomial
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
n✝ : ℕ
a✝¹ : R
a✝ : D ((aeval x) (C a✝¹ * X ^ n✝)) = (aeval x) (derivative (C a✝¹ * X ^ n✝)) • D x
⊢ D ((aeval x) (C a✝¹ * X ^ (n✝ + 1))) = (aeval x) (derivative (C a✝¹ * X ^ (n✝ + 1))) • D x

Proof state:
case h_add
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
p✝ q✝ : R[X]
a✝¹ : D ((aeval x) p✝) = (aeval x) (derivative p✝) • D x
a✝ : D ((aeval x) q✝) = (aeval x) (derivative q✝) • D x
⊢ D ((aeval x) (p✝ + q✝)) = (aeval x) (derivative (p✝ + q✝)) • D x

Tactic:
simp [add_smul, *]

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
n✝ : ℕ
a✝¹ : R
a✝ : D ((aeval x) (C a✝¹ * X ^ n✝)) = (aeval x) (derivative (C a✝¹ * X ^ n✝)) • D x
⊢ D ((aeval x) (C a✝¹ * X ^ (n✝ + 1))) = (aeval x) (derivative (C a✝¹ * X ^ (n✝ + 1))) • D x

Tactic:
simp [mul_smul, ← Nat.cast_smul_eq_nsmul A]

Result:
no goals
-- Mathlib/Analysis/Convex/Caratheodory.lean
theorem mem_convexHull_erase [DecidableEq E] {t : Finset E} (h : ¬AffineIndependent 𝕜 ((↑) : t → E))
    {x : E} (m : x ∈ convexHull 𝕜 (↑t : Set E)) :
    ∃ y : (↑t : Set E), x ∈ convexHull 𝕜 (↑(t.erase y) : Set E)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
⊢ ∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id

Tactic:
let k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
⊢ ∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id

Proof state:
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
⊢ ∑ y ∈ t.erase ↑⟨i₀, hi₀⟩, k y = 1

Tactic:
convert ksum

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∈ s
hge : 0 < g e
⊢ f i₀ / g i₀ ≤ f e / g e

Tactic:
exact w _ hes

Result:
no goals
-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
theorem _root_.Filter.HasBasis.compactConvergenceUniformity {ι : Type*} {pi : ι → Prop}
    {s : ι → Set (β × β)} (h : (𝓤 β).HasBasis pi s) :
    HasBasis (𝓤 C(α, β)) (fun p : Set α × ι => IsCompact p.1 ∧ pi p.2) fun p =>
      { fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2 }

Proof state:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u_1
pi : ι → Prop
s : ι → Set (β × β)
h : (𝓤 β).HasBasis pi s
⊢ (𝓤 C(α, β)).HasBasis (fun p => IsCompact p.1 ∧ pi p.2) fun p => {fg | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2}

Tactic:
rw [← isUniformEmbedding_toUniformOnFunIsCompact.comap_uniformity]

Result:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u_1
pi : ι → Prop
s : ι → Set (β × β)
h : (𝓤 β).HasBasis pi s
⊢ (Filter.comap (fun x => (x.1.toUniformOnFunIsCompact, x.2.toUniformOnFunIsCompact))
        (𝓤 (α →ᵤ[{K | IsCompact K}] β))).HasBasis
    (fun p => IsCompact p.1 ∧ pi p.2) fun p => {fg | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2}

Proof state:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u_1
pi : ι → Prop
s : ι → Set (β × β)
h : (𝓤 β).HasBasis pi s
⊢ (Filter.comap (fun x => (x.1.toUniformOnFunIsCompact, x.2.toUniformOnFunIsCompact))
        (𝓤 (α →ᵤ[{K | IsCompact K}] β))).HasBasis
    (fun p => IsCompact p.1 ∧ pi p.2) fun p => {fg | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2}

Tactic:
exact .comap _ <| UniformOnFun.hasBasis_uniformity_of_basis _ _ {K | IsCompact K}
  ⟨∅, isCompact_empty⟩ (directedOn_of_sup_mem fun _ _ ↦ IsCompact.union) h

Result:
no goals