harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem componentComplMk_eq_of_adj (G : SimpleGraph V) {v w : V} (vK : v ∉ K) (wK : w ∉ K)
    (a : G.Adj v w) : G.componentComplMk vK = G.componentComplMk wK

Proof state:
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ G.componentComplMk vK = G.componentComplMk wK

Tactic:
rw [ConnectedComponent.eq]

Result:
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ (induce Kᶜ G).Reachable ⟨v, vK⟩ ⟨w, wK⟩

Proof state:
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ (induce Kᶜ G).Reachable ⟨v, vK⟩ ⟨w, wK⟩

Tactic:
apply Adj.reachable

Result:
case h
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ (induce Kᶜ G).Adj ⟨v, vK⟩ ⟨w, wK⟩

Proof state:
case h
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ (induce Kᶜ G).Adj ⟨v, vK⟩ ⟨w, wK⟩

Tactic:
exact a

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem traverse_def (f : α → F β) (x : α) :
    ∀ xs : Vector α n, (x ::ᵥ xs).traverse f = cons <$> f x <*> xs.traverse f

Proof state:
case mk
F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Vector.traverse f (x ::ᵥ ⟨xs, ⋯⟩) = cons <$> f x <*> Vector.traverse f ⟨xs, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
⊢ ∀ (xs : Vector α n), Vector.traverse f (x ::ᵥ xs) = cons <$> f x <*> Vector.traverse f xs

Tactic:
rintro ⟨xs, rfl⟩

Result:
case mk
F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Vector.traverse f (x ::ᵥ ⟨xs, ⋯⟩) = cons <$> f x <*> Vector.traverse f ⟨xs, ⋯⟩
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma eHolderNorm_of_isEmpty [hX : IsEmpty X] :
    eHolderNorm r f = 0

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ eHolderNorm r f = 0

Tactic:
rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ ∀ b > ⊥, ∃ i, ∃ (_ : HolderWith i r f), ↑i < b

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ ∀ b > ⊥, ∃ i, ∃ (_ : HolderWith i r f), ↑i < b

Tactic:
exact fun ε hε => ⟨0, .of_isEmpty, hε⟩

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
theorem braiding_naturality_left {X Y : ModuleCat R} (f : X ⟶ Y) (Z : ModuleCat R) :
    f ▷ Z ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ Z ◁ f

Proof state:
R : Type u
inst✝ : CommRing R
X Y : ModuleCat R
f : X ⟶ Y
Z : ModuleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ (𝟙 Z ⊗ f)

Tactic:
apply braiding_naturality

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
X Y : ModuleCat R
f : X ⟶ Y
Z : ModuleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ Z ◁ f

Tactic:
simp_rw [← id_tensorHom]

Result:
R : Type u
inst✝ : CommRing R
X Y : ModuleCat R
f : X ⟶ Y
Z : ModuleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ (𝟙 Z ⊗ f)
-- Mathlib/Data/Fin/Basic.lean
theorem succ_castPred_le_iff {a b : Fin (n + 1)} (ha : a ≠ last n) :
    succ (a.castPred ha) ≤ b ↔ a < b

Proof state:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ (a.castPred ha).succ ≤ b ↔ a < b

Tactic:
rw [succ_castPred_eq_castPred_succ ha, castpred_succ_le_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Pi.map'_comp_map' {f : α → C} {g : β → C} {h : γ → C} [HasProduct f] [HasProduct g]
    [HasProduct h] (p : β → α) (p' : γ → β) (q : ∀ (b : β), f (p b) ⟶ g b)
    (q' : ∀ (c : γ), g (p' c) ⟶ h c) :
    Pi.map' p q ≫ Pi.map' p' q' = Pi.map' (p ∘ p') (fun c => q (p' c) ≫ q' c)

Proof state:
case h
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
p' : γ → β
q : (b : β) → f (p b) ⟶ g b
q' : (c : γ) → g (p' c) ⟶ h c
b✝ : γ
⊢ (map' p q ≫ map' p' q') ≫ π h b✝ = (map' (p ∘ p') fun c => q (p' c) ≫ q' c) ≫ π h b✝

Tactic:
simp

Result:
no goals

Proof state:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
p' : γ → β
q : (b : β) → f (p b) ⟶ g b
q' : (c : γ) → g (p' c) ⟶ h c
⊢ map' p q ≫ map' p' q' = map' (p ∘ p') fun c => q (p' c) ≫ q' c

Tactic:
ext

Result:
case h
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
p' : γ → β
q : (b : β) → f (p b) ⟶ g b
q' : (c : γ) → g (p' c) ⟶ h c
b✝ : γ
⊢ (map' p q ≫ map' p' q') ≫ π h b✝ = (map' (p ∘ p') fun c => q (p' c) ≫ q' c) ≫ π h b✝
-- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@[simp]
lemma free_δ_freeMk {X Y : Type u} (z : X ⊗ Y) :
    δ (free R) _ _ (freeMk z) = freeMk z.1 ⊗ₜ freeMk z.2

Proof state:
R : Type u
inst✝ : CommRing R
X Y : Type u
z : X ⊗ Y
⊢ (ConcreteCategory.hom (δ (free R) X Y)) (freeMk z) = freeMk z.1 ⊗ₜ[R] freeMk z.2

Tactic:
apply FreeMonoidal.μIso_inv_freeMk

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem add_left_aux1 (x y z : E) :
    ‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖
    = 2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖ = 2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)

Tactic:
convert parallelogram_identity (x + y + z) (x - z) using 4 <;> abel

Result:
no goals
-- Mathlib/Order/Filter/Ker.lean
@[simp] lemma ker_pure (a : α) : ker (pure a) = {a}

Proof state:
α : Type u_2
a : α
⊢ (pure a).ker = {a}

Tactic:
rw [← principal_singleton, ker_principal]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
/-- If `F : C ⥤ Dᵒᵖ` preserves finite products, then `F.leftOp : Cᵒᵖ ⥤ D` preserves finite
    coproducts. -/
lemma preservesFiniteCoproducts_leftOp (F : C ⥤ Dᵒᵖ) [PreservesFiniteProducts F] :
    PreservesFiniteCoproducts F.leftOp where
  preserves _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.leftOp

Tactic:
apply (config := { allowSynthFailures := true }) preservesColimitsOfShape_leftOp

Result:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Proof state:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Tactic:
exact preservesLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma IsUnramified.of_restrictScalars {w : InfinitePlace F} (h : IsUnramified k w) :
    IsUnramified K w

Proof state:
k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra k K
inst✝² : Algebra k F
inst✝¹ : Algebra K F
inst✝ : IsScalarTower k K F
w : InfinitePlace F
h : IsUnramified k w
⊢ IsUnramified K w

Tactic:
rw [InfinitePlace.isUnramified_iff_mult_le, ← h.eq, IsScalarTower.algebraMap_eq k K F,
  InfinitePlace.comap_comp]

Result:
k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra k K
inst✝² : Algebra k F
inst✝¹ : Algebra K F
inst✝ : IsScalarTower k K F
w : InfinitePlace F
h : IsUnramified k w
⊢ ((w.comap (algebraMap K F)).comap (algebraMap k K)).mult ≤ (w.comap (algebraMap K F)).mult

Proof state:
k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra k K
inst✝² : Algebra k F
inst✝¹ : Algebra K F
inst✝ : IsScalarTower k K F
w : InfinitePlace F
h : IsUnramified k w
⊢ ((w.comap (algebraMap K F)).comap (algebraMap k K)).mult ≤ (w.comap (algebraMap K F)).mult

Tactic:
exact InfinitePlace.mult_comap_le _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_emod_self (a : Int) : -a % a = 0

Proof state:
a : Int
⊢ -a % a = 0

Tactic:
rw [neg_emod, Int.sub_self, zero_emod]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem dvd_index_map {f : G →* G'} (hf : f.ker ≤ H) :
    H.index ∣ (H.map f).index

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ H.index * f.range.index

Tactic:
apply dvd_mul_right

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ (map f H).index

Tactic:
rw [index_map, sup_of_le_left hf]

Result:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ H.index * f.range.index
-- Mathlib/Data/Set/Prod.lean
theorem prod_range_univ_eq {m₁ : α → γ} :
    range m₁ ×ˢ (univ : Set β) = range fun p : α × β => (m₁ p.1, p.2) :=
  ext <| by simp [range]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m₁ : α → γ
⊢ ∀ (x : γ × β), x ∈ range m₁ ×ˢ univ ↔ x ∈ range fun p => (m₁ p.1, p.2)

Tactic:
simp [range]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem HasFPowerSeriesWithinOnBall.neg (hf : HasFPowerSeriesWithinOnBall f pf s x r) :
    HasFPowerSeriesWithinOnBall (-f) (-pf) s x r :=
  { r_le

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ pf.radius

Tactic:
exact hf.r_le

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ (-pf).radius

Tactic:
rw [pf.radius_neg]

Result:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ pf.radius
-- Mathlib/Data/Set/Lattice.lean
theorem image2_iUnion₂_right (s : Set α) (t : ∀ i, κ i → Set β) :
    image2 f s (⋃ (i) (j), t i j) = ⋃ (i) (j), image2 f s (t i j)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ image2 f s (⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, image2 f s (t i j)

Tactic:
simp_rw [image2_iUnion_right]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma coverEntropyInfEntourage_le_netEntropyInfEntourage (T : X → X) (F : Set X) {U : Set (X × X)}
    (U_rfl : idRel ⊆ U) (U_symm : SymmetricRel U) :
    coverEntropyInfEntourage T F (U ○ U) ≤ netEntropyInfEntourage T F U

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
⊢ coverEntropyInfEntourage T F (U ○ U) ≤ netEntropyInfEntourage T F U

Tactic:
refine (liminf_le_liminf) (Eventually.of_forall fun n ↦ ?_)

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(netMaxcard T F U n)).log / ↑n

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
⊢ (↑(coverMincard T F (U ○ U) n)).log / ↑n ≤ (↑(netMaxcard T F U n)).log / ↑n

Tactic:
apply div_le_div_right_of_nonneg (Nat.cast_nonneg' n) (log_monotone _)

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
⊢ ↑(coverMincard T F (U ○ U) n) ≤ ↑(netMaxcard T F U n)

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
⊢ ↑(coverMincard T F (U ○ U) n) ≤ ↑(netMaxcard T F U n)

Tactic:
exact ENat.toENNReal_le.2 (coverMincard_le_netMaxcard T F U_rfl U_symm n)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_comm (a b : Int) : a * b = b * a

Proof state:
a b : Int
⊢ a * b = b * a

Tactic:
cases a <;> cases b <;> simp [Nat.mul_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_add_one (ha : 0 ≤ a) : ⌈a + 1⌉₊ = ⌈a⌉₊ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ ⌈a + 1⌉₊ = ⌈a⌉₊ + 1

Tactic:
rw [cast_one.symm, ceil_add_nat ha 1]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsCoprime.pow_left_iff (hm : 0 < m) : IsCoprime (x ^ m) y ↔ IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
h : IsCoprime (∏ _x ∈ range m, x) y
⊢ IsCoprime x y

Tactic:
exact h.of_prod_left 0 (Finset.mem_range.mpr hm)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
⊢ IsCoprime (x ^ m) y ↔ IsCoprime x y

Tactic:
refine ⟨fun h ↦ ?_, IsCoprime.pow_left⟩

Result:
R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
h : IsCoprime (x ^ m) y
⊢ IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
h : IsCoprime (x ^ m) y
⊢ IsCoprime x y

Tactic:
rw [← Finset.card_range m, ← Finset.prod_const] at h

Result:
R : Type u
inst✝ : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
h : IsCoprime (∏ _x ∈ range m, x) y
⊢ IsCoprime x y
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem hasBasis_nhds_infty :
    (𝓝 (∞ : OnePoint X)).HasBasis (fun s : Set X => IsClosed s ∧ IsCompact s) fun s =>
      (↑) '' sᶜ ∪ {∞}

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (𝓝 ∞).HasBasis (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}

Tactic:
rw [nhds_infty_eq]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}

Tactic:
exact (hasBasis_coclosedCompact.map _).sup_pure _

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
lemma exists_compls_iff {p : α → Prop} : (∃ a ∈ sᶜˢ, p a) ↔ ∃ a ∈ s, p aᶜ

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
p : α → Prop
⊢ (∃ a ∈ sᶜˢ, p a) ↔ ∃ a ∈ s, p aᶜ

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem subset_eval_image_pi (ht : (s.pi t).Nonempty) (i : ι) : t i ⊆ eval i '' s.pi t

Proof state:
case intro
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
⊢ update f i y j ∈ t j

Tactic:
obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
ht : (s.pi t).Nonempty
i : ι
⊢ t i ⊆ eval i '' s.pi t

Tactic:
obtain ⟨f, hf⟩ := ht

Result:
case intro
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
⊢ t i ⊆ eval i '' s.pi t

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
ht : (s.pi t).Nonempty
i : ι
⊢ t i ⊆ eval i '' s.pi t

Tactic:
classical
obtain ⟨f, hf⟩ := ht
refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩
obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]

Result:
no goals

Proof state:
case intro
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
⊢ t i ⊆ eval i '' s.pi t

Tactic:
refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩

Result:
case intro
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ s.pi t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
⊢ update f i y j ∈ t j
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a fallback : α}
    {v : β k} :
    (m.insertIfNew k v).getKeyD a fallback =
      if k == a ∧ m.contains k = false then k else m.getKeyD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a fallback : α
v : β k
⊢ (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ m.contains k = false then k else m.getKeyD a fallback

Tactic:
simp_to_model [insertIfNew] using List.getKeyD_insertEntryIfNew

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_zero (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ 0 = 1

Tactic:
simp [rpow_def, cfc_const_one ℝ≥0 a]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem mem_closure_iff_infDist_zero (h : s.Nonempty) : x ∈ closure s ↔ infDist x s = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : s.Nonempty
⊢ x ∈ closure s ↔ infDist x s = 0

Tactic:
simp [mem_closure_iff_infEdist_zero, infDist, ENNReal.toReal_eq_zero_iff, infEdist_ne_top h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_nonpos_of_pi_div_two_le_of_le {x : ℝ} (hx₁ : π / 2 ≤ x) (hx₂ : x ≤ π + π / 2) :
    cos x ≤ 0 :=
  neg_nonneg.1 <| cos_pi_sub x ▸ cos_nonneg_of_mem_Icc ⟨by linarith, by linarith⟩

Proof state:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
⊢ π - x ≤ π / 2

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
⊢ -(π / 2) ≤ π - x

Tactic:
linarith

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma add_eq_min_iff : m + n = min m n ↔ m = 0 ∧ n = 0

Proof state:
m n : ℕ
⊢ m + n = min m n ↔ m = 0 ∧ n = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_subset_range (f : α → β) (s) : f '' s ⊆ range f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ range f

Tactic:
rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ

Tactic:
exact image_subset _ (subset_univ _)

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem linfty_opNNNorm_col (v : m → α) : ‖col ι v‖₊ = ‖v‖₊

Proof state:
m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (Finset.univ.sup fun i => ∑ j : ι, ‖col ι v i j‖₊) = Finset.univ.sup fun b => ‖v b‖₊

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ ‖col ι v‖₊ = ‖v‖₊

Tactic:
rw [linfty_opNNNorm_def, Pi.nnnorm_def]

Result:
m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (Finset.univ.sup fun i => ∑ j : ι, ‖col ι v i j‖₊) = Finset.univ.sup fun b => ‖v b‖₊
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem hsum_smul {x : HahnSeries Γ R} {s : SummableFamily Γ R α} :
    (x • s).hsum = x * s.hsum

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
s : SummableFamily Γ R α
⊢ (x • s).hsum = x * s.hsum

Tactic:
rw [hsum_smul_module, of_symm_smul_of_eq_mul]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
@[simp]
lemma comp_eqToHom_lift_iff {R S : 𝒮} {a' a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : a' = a) :
    p.IsHomLift f (eqToHom h ≫ φ) ↔ p.IsHomLift f φ where
  mp hφ'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a' a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : a' = a
hφ' : p.IsHomLift f (eqToHom h ≫ φ)
⊢ p.IsHomLift f φ

Tactic:
subst h

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a' b : 𝒳
f : R ⟶ S
φ : a' ⟶ b
hφ' : p.IsHomLift f (eqToHom ⋯ ≫ φ)
⊢ p.IsHomLift f φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a' b : 𝒳
f : R ⟶ S
φ : a' ⟶ b
hφ' : p.IsHomLift f (eqToHom ⋯ ≫ φ)
⊢ p.IsHomLift f φ

Tactic:
simpa using hφ'

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma toLeft_sdiff : (u \ v).toLeft = u.toLeft \ v.toLeft

Proof state:
case h
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u \ v).toLeft ↔ x ∈ u.toLeft \ v.toLeft

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u \ v).toLeft = u.toLeft \ v.toLeft

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u \ v).toLeft ↔ x ∈ u.toLeft \ v.toLeft
-- Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean
theorem to_affine_map_contLinear (f : V →L[R] W) : f.toContinuousAffineMap.contLinear = f

Proof state:
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedAddCommGroup W
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : V →L[R] W
⊢ f.toContinuousAffineMap.contLinear = f

Tactic:
ext

Result:
case h
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedAddCommGroup W
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : V →L[R] W
x✝ : V
⊢ f.toContinuousAffineMap.contLinear x✝ = f x✝

Proof state:
case h
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedAddCommGroup W
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : V →L[R] W
x✝ : V
⊢ f.toContinuousAffineMap.contLinear x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma top_mul_of_pos {x : EReal} (h : 0 < x) : ⊤ * x = ⊤

Proof state:
x : EReal
h : 0 < x
⊢ x * ⊤ = ⊤

Tactic:
exact mul_top_of_pos h

Result:
no goals

Proof state:
x : EReal
h : 0 < x
⊢ ⊤ * x = ⊤

Tactic:
rw [EReal.mul_comm]

Result:
x : EReal
h : 0 < x
⊢ x * ⊤ = ⊤
-- Mathlib/Computability/Primrec.lean
theorem nat_bodd : Primrec Nat.bodd :=
  (Primrec.beq.comp (nat_mod.comp .id (const 2)) (const 1)).of_eq fun n => by
    cases H : n.bodd <;> simp [Nat.mod_two_of_bodd, H]

Proof state:
n : ℕ
⊢ (id n % 2 == 1) = n.bodd

Tactic:
cases H : n.bodd <;> simp [Nat.mod_two_of_bodd, H]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma comapOn_isBase_iff :
    (N.comapOn E f).IsBase B ↔ N.IsBasis' (f '' B) (f '' E) ∧ B.InjOn f ∧ B ⊆ E

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
⊢ (N.comapOn E f).IsBase B ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E

Tactic:
rw [comapOn, isBase_restrict_iff', comap_isBasis'_iff]

Result:
no goals