harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Connected/Basic.lean
theorem IsPreconnected.subset_or_subset (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v)
    (hsuv : s ⊆ u ∪ v) (hs : IsPreconnected s) : s ⊆ u ∨ s ⊆ v

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
obtain hsu | hsu := (s ∩ u).eq_empty_or_nonempty

Result:
case inl
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : s ∩ u = ∅
⊢ s ⊆ u ∨ s ⊆ v

case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : (s ∩ u).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
case inl
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : s ∩ u = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
exact Or.inr ((Set.disjoint_iff_inter_eq_empty.2 hsu).subset_right_of_subset_union hsuv)

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : IsPreconnected s
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
specialize hs u v hu hv hsuv

Result:
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : Disjoint s ∅ → Disjoint s v
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
exact Or.inl ((hs s.disjoint_empty).subset_left_of_subset_union hsuv)

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : ¬(s ∩ (u ∩ v)).Nonempty → ¬(s ∩ v).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
simp_rw [Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty,
  disjoint_iff_inter_eq_empty.1 huv] at hs

Result:
case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : Disjoint s ∅ → Disjoint s v
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
hsu : (s ∩ u).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
replace hs := mt (hs hsu)

Result:
case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : ¬(s ∩ (u ∩ v)).Nonempty → ¬(s ∩ v).Nonempty
⊢ s ⊆ u ∨ s ⊆ v
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
lemma valuation_coe_nonneg : 0 ≤ (x : ℚ_[p]).valuation

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0 ≤ (↑0).valuation

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ 0 ≤ (↑x).valuation

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0 ≤ (↑0).valuation

case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ 0 ≤ (↑x).valuation

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ 0 ≤ (↑x).valuation

Tactic:
have := x.2

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
this : ‖↑x‖ ≤ 1
⊢ 0 ≤ (↑x).valuation

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
this : ‖↑x‖ ≤ 1
⊢ 0 ≤ (↑x).valuation

Tactic:
rwa [Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx, zpow_le_one_iff_right₀, neg_nonpos]
  at this

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
this : ↑p ^ (-(↑x).valuation) ≤ 1
⊢ 1 < ↑p

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
this : ↑p ^ (-(↑x).valuation) ≤ 1
⊢ 1 < ↑p

Tactic:
exact mod_cast hp.out.one_lt

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem compl_not_mem_iff : sᶜ ∉ f ↔ s ∈ f :=
  ⟨fun hsc =>
    le_principal_iff.1 <|
      f.le_of_inf_neBot ⟨fun h => hsc <| mem_of_eq_bot <| by rwa [compl_compl]⟩,
    compl_not_mem⟩

Proof state:
α : Type u
f : Ultrafilter α
s : Set α
hsc : sᶜ ∉ f
h : ↑f ⊓ 𝓟 s = ⊥
⊢ ↑f ⊓ 𝓟 sᶜᶜ = ⊥

Tactic:
rwa [compl_compl]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
@[simp] lemma minSmoothness_of_isRCLikeNormedField [h : IsRCLikeNormedField 𝕜] {n : WithTop ℕ∞} :
    minSmoothness 𝕜 n = n

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
h : IsRCLikeNormedField 𝕜
n : WithTop ℕ∞
⊢ minSmoothness 𝕜 n = n

Tactic:
simp [minSmoothness, h]

Result:
no goals
-- Mathlib/Data/List/Perm/Basic.lean
theorem perm_option_toList {o₁ o₂ : Option α} : o₁.toList ~ o₂.toList ↔ o₁ = o₂

Proof state:
α : Type u_1
o₁ o₂ : Option α
p : o₁.toList ~ o₂.toList
⊢ o₁ = o₂

Tactic:
rcases o₁ with - | a <;> rcases o₂ with - | b

Result:
case none.none
α : Type u_1
p : none.toList ~ none.toList
⊢ none = none

case none.some
α : Type u_1
b : α
p : none.toList ~ (some b).toList
⊢ none = some b

case some.none
α : Type u_1
a : α
p : (some a).toList ~ none.toList
⊢ some a = none

case some.some
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ some a = some b

Proof state:
α : Type u_1
o₁ o₂ : Option α
⊢ o₁.toList ~ o₂.toList ↔ o₁ = o₂

Tactic:
refine ⟨fun p => ?_, fun e => e ▸ Perm.refl _⟩

Result:
α : Type u_1
o₁ o₂ : Option α
p : o₁.toList ~ o₂.toList
⊢ o₁ = o₂

Proof state:
case some.some
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ some a = some b

Tactic:
exact Option.mem_toList.1 (p.symm.subset <| by simp)

Result:
no goals

Proof state:
case none.some
α : Type u_1
b : α
p : none.toList ~ (some b).toList
⊢ none = some b

Tactic:
cases p.length_eq

Result:
no goals

Proof state:
case none.none
α : Type u_1
p : none.toList ~ none.toList
⊢ none = none

Tactic:
rfl

Result:
no goals

Proof state:
case some.none
α : Type u_1
a : α
p : (some a).toList ~ none.toList
⊢ some a = none

Tactic:
cases p.length_eq

Result:
no goals

Proof state:
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ b ∈ (some b).toList

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph0_lt_aleph_one : ℵ₀ < ℵ₁

Proof state:
⊢ ℵ₀ < ℵ_ 1

Tactic:
rw [← succ_aleph0]

Result:
⊢ ℵ₀ < succ ℵ₀

Proof state:
⊢ ℵ₀ < succ ℵ₀

Tactic:
apply lt_succ

Result:
no goals
-- Mathlib/Order/Filter/Ker.lean
theorem ker_iSup (f : ι → Filter α) : ker (⨆ i, f i) = ⋃ i, ker (f i)

Proof state:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
s : ι → Set α
hsf : ∀ (i : ι), s i ∈ f i
hxs : ∀ (i : ι), x ∉ s i
⊢ ∃ s ∈ ⨆ i, f i, x ∉ s

Tactic:
refine ⟨⋃ i, s i, ?_, by simpa⟩

Result:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
s : ι → Set α
hsf : ∀ (i : ι), s i ∈ f i
hxs : ∀ (i : ι), x ∉ s i
⊢ ⋃ i, s i ∈ ⨆ i, f i

Proof state:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
s : ι → Set α
hsf : ∀ (i : ι), s i ∈ f i
hxs : ∀ (i : ι), x ∉ s i
⊢ ⋃ i, s i ∈ ⨆ i, f i

Tactic:
exact mem_iSup.2 fun i ↦ mem_of_superset (hsf i) (subset_iUnion s i)

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : ∀ s ∈ ⨆ i, f i, x ∈ s
⊢ ∃ i, ∀ s ∈ f i, x ∈ s

Tactic:
contrapose! hx

Result:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : ∀ (i : ι), ∃ s ∈ f i, x ∉ s
⊢ ∃ s ∈ ⨆ i, f i, x ∉ s

Proof state:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : ∀ (i : ι), ∃ s ∈ f i, x ∉ s
⊢ ∃ s ∈ ⨆ i, f i, x ∉ s

Tactic:
choose s hsf hxs using hx

Result:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
s : ι → Set α
hsf : ∀ (i : ι), s i ∈ f i
hxs : ∀ (i : ι), x ∉ s i
⊢ ∃ s ∈ ⨆ i, f i, x ∉ s

Proof state:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
s : ι → Set α
hsf : ∀ (i : ι), s i ∈ f i
hxs : ∀ (i : ι), x ∉ s i
⊢ x ∉ ⋃ i, s i

Tactic:
simpa

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : x ∈ (⨆ i, f i).ker
⊢ x ∈ ⋃ i, (f i).ker

Tactic:
simp only [mem_iUnion, mem_ker] at hx ⊢

Result:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : ∀ s ∈ ⨆ i, f i, x ∈ s
⊢ ∃ i, ∀ s ∈ f i, x ∈ s

Proof state:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (⨆ i, f i).ker = ⋃ i, (f i).ker

Tactic:
refine subset_antisymm (fun x hx ↦ ?_) ker_mono.le_map_iSup

Result:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : x ∈ (⨆ i, f i).ker
⊢ x ∈ ⋃ i, (f i).ker
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mkRat_mul_left {a : Nat} (a0 : a ≠ 0) : mkRat (↑a * n) (a * d) = mkRat n d

Proof state:
n : Int
d a : Nat
a0 : a ≠ 0
d0 : d = 0
⊢ mkRat (↑a * n) (a * d) = mkRat n d

Tactic:
simp [d0]

Result:
no goals

Proof state:
n : Int
d a : Nat
a0 : a ≠ 0
⊢ mkRat (↑a * n) (a * d) = mkRat n d

Tactic:
if d0 : d = 0 then simp [d0] else
rw [← normalize_eq_mkRat d0, ← normalize_mul_left d0 a0, normalize_eq_mkRat]

Result:
no goals

Proof state:
n : Int
d a : Nat
a0 : a ≠ 0
d0 : ¬d = 0
⊢ mkRat (↑a * n) (a * d) = mkRat n d

Tactic:
rw [← normalize_eq_mkRat d0, ← normalize_mul_left d0 a0, normalize_eq_mkRat]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem eq_of_dist_eq_zero (x y : ∀ n, E n) (hxy : dist x y = 0) : x = y

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
⊢ x = y

Tactic:
rcases eq_or_ne x y with (rfl | h)

Result:
case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
hxy : dist x x = 0
⊢ x = x

case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
h : x ≠ y
⊢ x = y

Proof state:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
h : x ≠ y
⊢ x = y

Tactic:
simp [dist_eq_of_ne h] at hxy

Result:
no goals

Proof state:
case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
hxy : dist x x = 0
⊢ x = x

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma birkhoffSet_sup (a b : α) : birkhoffSet (a ⊔ b) = birkhoffSet a ∪ birkhoffSet b

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ birkhoffSet (a ⊔ b) = birkhoffSet a ∪ birkhoffSet b

Tactic:
unfold OrderEmbedding.birkhoffSet

Result:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ (if h : IsEmpty α then ofIsEmpty
      else
        let_fun this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊔ b) =
    (if h : IsEmpty α then ofIsEmpty
        else
          let_fun this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∪
      (if h : IsEmpty α then ofIsEmpty
        else
          let_fun this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Proof state:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ (if h : IsEmpty α then ofIsEmpty
      else
        let_fun this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊔ b) =
    (if h : IsEmpty α then ofIsEmpty
        else
          let_fun this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∪
      (if h : IsEmpty α then ofIsEmpty
        else
          let_fun this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Tactic:
split <;> simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem self_mem_cycle_factors_commute {g c : Perm α}
    (hc : c ∈ g.cycleFactorsFinset) : Commute c g

Proof state:
case hk
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
⊢ Commute c c'

Tactic:
by_cases hcc' : c = c'

Result:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : c = c'
⊢ Commute c c'

case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ Commute c c'

Proof state:
case hk
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ ∀ c_1 ∈ g.cycleFactorsFinset, Commute c c_1

Tactic:
intro c' hc'

Result:
case hk
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
⊢ Commute c c'

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute c g

Tactic:
apply commute_of_mem_cycleFactorsFinset_commute

Result:
case hk
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ ∀ c_1 ∈ g.cycleFactorsFinset, Commute c c_1

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ c ≠ c'

Tactic:
exact hcc'

Result:
no goals

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ Commute c c'

Tactic:
apply g.cycleFactorsFinset_mem_commute hc hc'

Result:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ c ≠ c'

Proof state:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : c = c'
⊢ Commute c c'

Tactic:
rw [hcc']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FinallySmall.lean
theorem initiallySmall_iff_exists_small_weakly_initial_set [IsCofilteredOrEmpty J] :
    InitiallySmall.{v} J ↔ ∃ (s : Set J) (_ : Small.{v} s), ∀ i, ∃ j ∈ s, Nonempty (j ⟶ i)

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsCofilteredOrEmpty J
h : ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
⊢ InitiallySmall J

Tactic:
rcases h with ⟨s, hs, hs'⟩

Result:
case intro.intro
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsCofilteredOrEmpty J
s : Set J
hs : Small.{v, u} ↑s
hs' : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
⊢ InitiallySmall J

Proof state:
case intro.intro
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsCofilteredOrEmpty J
s : Set J
hs : Small.{v, u} ↑s
hs' : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
⊢ InitiallySmall J

Tactic:
exact initiallySmall_of_small_weakly_initial_set s hs'

Result:
no goals

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsCofilteredOrEmpty J
⊢ InitiallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)

Tactic:
refine ⟨fun _ => InitiallySmall.exists_small_weakly_initial_set _, fun h => ?_⟩

Result:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsCofilteredOrEmpty J
h : ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
⊢ InitiallySmall J
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whisker_assoc (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
    (X ◁ f) ▷ Z = (α_ X Y Z).hom ≫ X ◁ f ▷ Z ≫ (α_ X Y' Z).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (𝟙 X ⊗ f) ⊗ 𝟙 Z = (α_ X Y Z).hom ≫ (𝟙 X ⊗ f ⊗ 𝟙 Z) ≫ (α_ X Y' Z).inv

Tactic:
rw [← assoc, ← associator_naturality]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (𝟙 X ⊗ f) ⊗ 𝟙 Z = (((𝟙 X ⊗ f) ⊗ 𝟙 Z) ≫ (α_ X Y' Z).hom) ≫ (α_ X Y' Z).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (X ◁ f) ▷ Z = (α_ X Y Z).hom ≫ X ◁ f ▷ Z ≫ (α_ X Y' Z).inv

Tactic:
simp only [← id_tensorHom, ← tensorHom_id]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (𝟙 X ⊗ f) ⊗ 𝟙 Z = (α_ X Y Z).hom ≫ (𝟙 X ⊗ f ⊗ 𝟙 Z) ≫ (α_ X Y' Z).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (𝟙 X ⊗ f) ⊗ 𝟙 Z = (((𝟙 X ⊗ f) ⊗ 𝟙 Z) ≫ (α_ X Y' Z).hom) ≫ (α_ X Y' Z).inv

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem not_step_nil : ¬Step [] L

Proof state:
α : Type u
L L' : List (α × Bool)
h' : [] = L'
h : Step L' L
⊢ False

Tactic:
rcases h with - | ⟨L₁, L₂⟩

Result:
case not
α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
h' : [] = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
⊢ False

Proof state:
α : Type u
L : List (α × Bool)
⊢ ¬Step [] L

Tactic:
generalize h' : [] = L'

Result:
α : Type u
L L' : List (α × Bool)
h' : [] = L'
⊢ ¬Step L' L

Proof state:
case not
α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
h' : [] = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
⊢ False

Tactic:
simp [List.nil_eq_append_iff] at h'

Result:
no goals

Proof state:
α : Type u
L L' : List (α × Bool)
h' : [] = L'
⊢ ¬Step L' L

Tactic:
intro h

Result:
α : Type u
L L' : List (α × Bool)
h' : [] = L'
h : Step L' L
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_one_left : logb 1 x = 0

Proof state:
x : ℝ
⊢ logb 1 x = 0

Tactic:
simp only [← log_div_log, log_one, div_zero]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem any_singleton {P : α → Prop} {x : α} : Any P (singleton x) ↔ P x :=
  ⟨by rintro (⟨⟨⟩⟩ | h | ⟨⟨⟩⟩); exact h, fun h => Or.inr (Or.inl h)⟩

Proof state:
case inr.inl
α : Type u_1
P : α → Prop
x : α
h : P x
⊢ P x

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
x : α
⊢ Any P {x} → P x

Tactic:
rintro (⟨⟨⟩⟩ | h | ⟨⟨⟩⟩)

Result:
case inr.inl
α : Type u_1
P : α → Prop
x : α
h : P x
⊢ P x
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_interpolate_not_at_node' (hvs : Set.InjOn v s) (hs : s.Nonempty)
    (hx : ∀ i ∈ s, x ≠ v i) :
    eval x (interpolate s v r) =
      (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) /
        ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
hx : ∀ i ∈ s, x ≠ v i
⊢ eval x ((interpolate s v) r) =
    (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹

Tactic:
rw [← div_one (eval x (interpolate s v r)), ← @eval_one _ _ x, ← interpolate_one hvs hs,
  eval_interpolate_not_at_node r hx, eval_interpolate_not_at_node 1 hx]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
hx : ∀ i ∈ s, x ≠ v i
⊢ (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) /
      (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * 1 i) =
    (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
hx : ∀ i ∈ s, x ≠ v i
⊢ (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) /
      (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * 1 i) =
    (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹

Tactic:
simp only [mul_div_mul_left _ _ (eval_nodal_not_at_node hx), Pi.one_apply, mul_one]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem exists_inv_nat_lt {a : ℝ≥0∞} (h : a ≠ 0) : ∃ n : ℕ, (n : ℝ≥0∞)⁻¹ < a :=
  inv_inv a ▸ by simp only [ENNReal.inv_lt_inv, ENNReal.exists_nat_gt (inv_ne_top.2 h)]

Proof state:
a : ℝ≥0∞
h : a ≠ 0
⊢ ∃ n, (↑n)⁻¹ < a⁻¹⁻¹

Tactic:
simp only [ENNReal.inv_lt_inv, ENNReal.exists_nat_gt (inv_ne_top.2 h)]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem mem_span_latticeBasis {x : (mixedSpace K)} :
    x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔
      x ∈ mixedEmbedding.integerLattice K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ Set.range ⇑(latticeBasis K) = ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(integralBasis K)

Tactic:
rw [← Set.range_comp]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ Set.range ⇑(latticeBasis K) = Set.range (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap ∘ ⇑(integralBasis K))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∃ a, (mixedEmbedding K).toIntAlgHom.toLinearMap ((algebraMap (𝓞 K) K) a) = x) ↔ x ∈ mixedEmbedding.integerLattice K

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))) ↔
    x ∈ mixedEmbedding.integerLattice K

Tactic:
simp only [Set.mem_image, SetLike.mem_coe, mem_span_integralBasis K,
  RingHom.mem_range, exists_exists_eq_and]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∃ a, (mixedEmbedding K).toIntAlgHom.toLinearMap ((algebraMap (𝓞 K) K) a) = x) ↔ x ∈ mixedEmbedding.integerLattice K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ x ∈ Submodule.span ℤ (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(integralBasis K)) ↔
    x ∈ mixedEmbedding.integerLattice K

Tactic:
rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))) ↔
    x ∈ mixedEmbedding.integerLattice K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(latticeBasis K)) ↔ x ∈ mixedEmbedding.integerLattice K

Tactic:
rw [show Set.range (latticeBasis K) =
    (mixedEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by
  rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ x ∈ Submodule.span ℤ (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(integralBasis K)) ↔
    x ∈ mixedEmbedding.integerLattice K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ Set.range ⇑(latticeBasis K) = Set.range (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap ∘ ⇑(integralBasis K))

Tactic:
exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))

Result:
no goals
-- Mathlib/SetTheory/Descriptive/Tree.lean
lemma mem_of_append {x y : List A} (h : x ++ y ∈ T) : x ∈ T

Proof state:
case nil
A : Type u_1
T : ↥(tree A)
x : List A
h : x ++ [] ∈ T
⊢ x ∈ T

Tactic:
simpa using h

Result:
no goals

Proof state:
case cons
A : Type u_1
T : ↥(tree A)
y : A
ys : List A
ih : ∀ {x : List A}, x ++ ys ∈ T → x ∈ T
x : List A
h : x ++ y :: ys ∈ T
⊢ x ∈ T

Tactic:
exact T.prop (ih (by simpa))

Result:
no goals

Proof state:
A : Type u_1
T : ↥(tree A)
x y : List A
h : x ++ y ∈ T
⊢ x ∈ T

Tactic:
induction' y with y ys ih generalizing x

Result:
case nil
A : Type u_1
T : ↥(tree A)
x : List A
h : x ++ [] ∈ T
⊢ x ∈ T

case cons
A : Type u_1
T : ↥(tree A)
y : A
ys : List A
ih : ∀ {x : List A}, x ++ ys ∈ T → x ∈ T
x : List A
h : x ++ y :: ys ∈ T
⊢ x ∈ T

Proof state:
A : Type u_1
T : ↥(tree A)
y : A
ys : List A
ih : ∀ {x : List A}, x ++ ys ∈ T → x ∈ T
x : List A
h : x ++ y :: ys ∈ T
⊢ x ++ [?m.896] ++ ys ∈ T

Tactic:
simpa

Result:
no goals