harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Pow.lean
theorem two_pow_pred_sub_two_pow' {w : Nat} (h : 0 < w) :
    (2 : Int) ^ (w - 1) - (2 : Int) ^ w = - (2 : Int) ^ (w - 1)

Proof state:
w : Nat
h : 0 < w
⊢ ↑(2 ^ (w - 1)) - ↑(2 ^ (w - 1) + 2 ^ (w - 1)) = -↑(2 ^ (w - 1))

Tactic:
simp [h]

Result:
no goals

Proof state:
w : Nat
h : 0 < w
⊢ ↑(2 ^ (w - 1)) - ↑(2 ^ w) = -↑(2 ^ (w - 1))

Tactic:
rw [← Nat.two_pow_pred_add_two_pow_pred h]

Result:
w : Nat
h : 0 < w
⊢ ↑(2 ^ (w - 1)) - ↑(2 ^ (w - 1) + 2 ^ (w - 1)) = -↑(2 ^ (w - 1))

Proof state:
w : Nat
h : 0 < w
⊢ 2 ^ (w - 1) - 2 ^ w = -2 ^ (w - 1)

Tactic:
norm_cast

Result:
w : Nat
h : 0 < w
⊢ ↑(2 ^ (w - 1)) - ↑(2 ^ w) = -↑(2 ^ (w - 1))
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem X_ne_C [Nontrivial R] (a : R) : X ≠ C a

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
⊢ X ≠ C a

Tactic:
intro he

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
he : X = C a
⊢ False

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
he : X = C a
⊢ False

Tactic:
simpa using monomial_eq_monomial_iff.1 he

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertEntryIfNew_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a)} {k : α}
    {v : β k} (h : containsKey k l = false) : insertEntryIfNew k v l = ⟨k, v⟩ :: l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = false
⊢ insertEntryIfNew k v l = ⟨k, v⟩ :: l

Tactic:
simp_all [insertEntryIfNew]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepSets.iInter {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} (h : ∃ n, IndepSets (s n) s' κ μ) :
    IndepSets (⋂ n, s n) s' κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∃ n, IndepSets (s n) s' κ μ
⊢ IndepSets (⋂ n, s n) s' κ μ

Tactic:
intro t1 t2 ht1 ht2

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∃ n, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ n, s n
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∃ n, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ n, s n
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
obtain ⟨n, h⟩ := h

Result:
case intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ n, s n
ht2 : t2 ∈ s'
n : ι
h : IndepSets (s n) s' κ μ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
case intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ n, s n
ht2 : t2 ∈ s'
n : ι
h : IndepSets (s n) s' κ μ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
exact h t1 t2 (Set.mem_iInter.mp ht1 n) ht2

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem comap_exp_nhdsNE : comap exp (𝓝[≠] 0) = comap re atBot

Proof state:
this : (cexp ⁻¹' {0})ᶜ = Set.univ
⊢ comap cexp (𝓝[≠] 0) = comap re atBot

Tactic:
simp [nhdsWithin, comap_exp_nhds_zero, this]

Result:
no goals

Proof state:
⊢ comap cexp (𝓝[≠] 0) = comap re atBot

Tactic:
have : (exp ⁻¹' {0})ᶜ = Set.univ := eq_univ_of_forall exp_ne_zero

Result:
this : (cexp ⁻¹' {0})ᶜ = Set.univ
⊢ comap cexp (𝓝[≠] 0) = comap re atBot
-- Mathlib/Order/SupIndep.lean
theorem iSupIndep_iff_supIndep_univ [Fintype ι] {f : ι → α} :
    iSupIndep f ↔ Finset.univ.SupIndep f

Proof state:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : Fintype ι
f : ι → α
⊢ iSupIndep f ↔ Finset.univ.SupIndep f

Tactic:
classical
  simp [Finset.supIndep_iff_disjoint_erase, iSupIndep, Finset.sup_eq_iSup]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : Fintype ι
f : ι → α
⊢ iSupIndep f ↔ Finset.univ.SupIndep f

Tactic:
simp [Finset.supIndep_iff_disjoint_erase, iSupIndep, Finset.sup_eq_iSup]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
theorem mem_upShadow_iff_exists_mem_card_add :
    s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #s

Proof state:
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s) → ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s

Tactic:
rintro ⟨t, ht, hts, hcard⟩

Result:
case succ.mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
⊢ ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s

Proof state:
case succ.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
⊢ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

Tactic:
obtain ⟨u, hu, hut, hcardtu⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 ht

Result:
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : #t + k = #s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : #t = #u + 1
⊢ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Sigma.map'_eq {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g]
    {p p' : α → β} {q : ∀ (a : α), f a ⟶ g (p a)} {q' : ∀ (a : α), f a ⟶ g (p' a)}
    (hp : p = p') (hq : ∀ (a : α), q a ≫ eqToHom (hp ▸ rfl) = q' a) :
    Sigma.map' p q = Sigma.map' p' q'

Proof state:
β : Type w
α : Type w₂
C : Type u
inst✝² : Category.{v, u} C
f : α → C
g : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct g
p p' : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (a : α) → f a ⟶ g (p' a)
hp : p = p'
hq : ∀ (a : α), q a ≫ eqToHom ⋯ = q' a
⊢ map' p q = map' p' q'

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_add' (a m n : Nat) : a ^ (m + n) = a ^ n * a ^ m

Proof state:
a m n : Nat
⊢ a ^ (m + n) = a ^ n * a ^ m

Tactic:
rw [← Nat.pow_add, Nat.add_comm]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Symmetric.lean
theorem lift_spec [HasReverse V'] (φ : Prefunctor V V') :
    Symmetrify.of.comp (Symmetrify.lift φ) = φ

Proof state:
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ of ⋙q lift φ = φ

Tactic:
fapply Prefunctor.ext

Result:
case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X

case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Proof state:
case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X

Tactic:
rintro X

Result:
case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X : V
⊢ (of ⋙q lift φ).obj X = φ.obj X

Proof state:
case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
rintro X Y f

Result:
case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X Y : V
f : X ⟶ Y
⊢ (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Proof state:
case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X Y : V
f : X ⟶ Y
⊢ (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
rfl

Result:
no goals

Proof state:
case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X : V
⊢ (of ⋙q lift φ).obj X = φ.obj X

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem jordan_holder (s₁ s₂ : CompositionSeries X)
    (hb : s₁.head = s₂.head) (ht : s₁.last = s₂.last) :
    Equivalent s₁ s₂

Proof state:
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), head s₁ = head s₂ → last s₁ = last s₂ → s₁.length = n → s₁.Equivalent s₂
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hle : s₁.length = n + 1
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : head t = head s₁
htl : t.length + 1 = s₁.length
htt : last t = (eraseLast s₂).last
hteq : s₁.Equivalent (snoc t (last s₁) ⋯)
this : t.Equivalent (eraseLast s₂)
⊢ Equivalent (snoc t (last s₁) ⋯) ((eraseLast s₂).snoc (last s₂) ⋯)

Tactic:
simp only [ht]

Result:
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), head s₁ = head s₂ → last s₁ = last s₂ → s₁.length = n → s₁.Equivalent s₂
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hle : s₁.length = n + 1
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : head t = head s₁
htl : t.length + 1 = s₁.length
htt : last t = (eraseLast s₂).last
hteq : s₁.Equivalent (snoc t (last s₁) ⋯)
this : t.Equivalent (eraseLast s₂)
⊢ Equivalent (snoc t (last s₂) ⋯) ((eraseLast s₂).snoc (last s₂) ⋯)

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), head s₁ = head s₂ → last s₁ = last s₂ → s₁.length = n → s₁.Equivalent s₂
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hle : s₁.length = n + 1
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : head t = head s₁
htl : t.length + 1 = s₁.length
htt : last t = (eraseLast s₂).last
hteq : s₁.Equivalent (snoc t (last s₁) ⋯)
this : t.Equivalent (eraseLast s₂)
⊢ Iso (last t, last s₂) ((eraseLast s₂).last, last s₂)

Tactic:
simpa [htt] using (isMaximal_eraseLast_last h0s₂).iso_refl

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
theorem algebraMap_gradedMul (r : R) (x : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i)) :
    gradedMul R 𝒜 ℬ (algebraMap R _ r ⊗ₜ 1) x = r • x

Proof state:
case a.H.h.H.h
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
⊢ (-1) ^ (0 * ia) •
      ((algebraMap R (DirectSum ι 𝒜)) r * (lof R ι 𝒜 ia) a) ⊗ₜ[R]
        ((lof R ι ℬ 0) GradedMonoid.GOne.one * (lof R ι ℬ ib) b) =
    r • (lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b

Tactic:
rw [zero_mul, uzpow_zero, one_smul, smul_tmul']

Result:
case a.H.h.H.h
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
⊢ ((algebraMap R (DirectSum ι 𝒜)) r * (lof R ι 𝒜 ia) a) ⊗ₜ[R] ((lof R ι ℬ 0) GradedMonoid.GOne.one * (lof R ι ℬ ib) b) =
    (r • (lof R ι 𝒜 ia) a) ⊗ₜ[R] (lof R ι ℬ ib) b
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem tag_mem (ν : ι → ℤ) :
    tag n ν ∈ box n ν

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
⊢ ↑(ν x✝) / ↑n < tag n ν x✝ ∧ tag n ν x✝ ≤ (↑(ν x✝) + 1) / ↑n

Tactic:
rw [tag, add_div]

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
⊢ ↑(ν x✝) / ↑n < ↑(ν x✝) / ↑n + 1 / ↑n ∧ ↑(ν x✝) / ↑n + 1 / ↑n ≤ ↑(ν x✝) / ↑n + 1 / ↑n

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
h : 0 < ↑n
⊢ 0 < 1 / ↑n

Tactic:
positivity

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
⊢ ↑(ν x✝) / ↑n < ↑(ν x✝) / ↑n + 1 / ↑n ∧ ↑(ν x✝) / ↑n + 1 / ↑n ≤ ↑(ν x✝) / ↑n + 1 / ↑n

Tactic:
have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
h : 0 < ↑n
⊢ ↑(ν x✝) / ↑n < ↑(ν x✝) / ↑n + 1 / ↑n ∧ ↑(ν x✝) / ↑n + 1 / ↑n ≤ ↑(ν x✝) / ↑n + 1 / ↑n

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
⊢ tag n ν ∈ box n ν

Tactic:
refine mem_box_iff.mpr fun _ ↦ ?_

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
⊢ ↑(ν x✝) / ↑n < tag n ν x✝ ∧ tag n ν x✝ ≤ (↑(ν x✝) + 1) / ↑n

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x✝ : ι
h : 0 < ↑n
⊢ ↑(ν x✝) / ↑n < ↑(ν x✝) / ↑n + 1 / ↑n ∧ ↑(ν x✝) / ↑n + 1 / ↑n ≤ ↑(ν x✝) / ↑n + 1 / ↑n

Tactic:
exact ⟨lt_add_of_pos_right _ (by positivity), le_rfl⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma Icc_isBoundaryPoint_top : (𝓡∂ 1).IsBoundaryPoint (⊤ : Set.Icc x y)

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ y ≤ ↑⊤

Tactic:
norm_num

Result:
no goals

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccRightChart x y).extend (𝓡∂ 1)) ⊤ ∈ frontier (range ↑(𝓡∂ 1))

Tactic:
exact IccRightChart_extend_top_mem_frontier

Result:
no goals

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ (𝓡∂ 1).IsBoundaryPoint ⊤

Tactic:
rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt,
  Icc_chartedSpaceChartAt_of_top_le (by norm_num)]

Result:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccRightChart x y).extend (𝓡∂ 1)) ⊤ ∈ frontier (range ↑(𝓡∂ 1))
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@[simp]
lemma toMvPolynomial_one [DecidableEq n] : (1 : Matrix n n R).toMvPolynomial = X

Proof state:
case h.h₀
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i j : n
hj : j ≠ i
⊢ (monomial (Finsupp.single j 1)) (1 i j) = 0

Tactic:
simp only [one_apply_ne hj.symm, map_zero]

Result:
no goals

Proof state:
case h.h₀
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial (Finsupp.single b 1)) (1 i b) = 0

Tactic:
rintro j - hj

Result:
case h.h₀
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i j : n
hj : j ≠ i
⊢ (monomial (Finsupp.single j 1)) (1 i j) = 0

Proof state:
case h.h₁
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ i ∉ Finset.univ → (monomial (Finsupp.single i 1)) (1 i i) = 0

Tactic:
intro h

Result:
case h.h₁
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
h : i ∉ Finset.univ
⊢ (monomial (Finsupp.single i 1)) (1 i i) = 0

Proof state:
case h
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ toMvPolynomial 1 i = X i

Tactic:
rw [toMvPolynomial, Finset.sum_eq_single i]

Result:
case h
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ (monomial (Finsupp.single i 1)) (1 i i) = X i

case h.h₀
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial (Finsupp.single b 1)) (1 i b) = 0

case h.h₁
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ i ∉ Finset.univ → (monomial (Finsupp.single i 1)) (1 i i) = 0

Proof state:
case h.h₁
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
h : i ∉ Finset.univ
⊢ (monomial (Finsupp.single i 1)) (1 i i) = 0

Tactic:
exact (h (Finset.mem_univ _)).elim

Result:
no goals

Proof state:
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
⊢ toMvPolynomial 1 = X

Tactic:
ext i : 1

Result:
case h
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ toMvPolynomial 1 i = X i

Proof state:
case h
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ (monomial (Finsupp.single i 1)) (1 i i) = X i

Tactic:
simp only [one_apply_eq, ← C_mul_X_eq_monomial, C_1, one_mul]

Result:
no goals
-- Mathlib/Topology/Category/Compactum.lean
theorem continuous_of_hom {X Y : Compactum} (f : X ⟶ Y) : Continuous f

Proof state:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ ↑g ≤ 𝓝 x

Tactic:
apply h

Result:
no goals

Proof state:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))

Tactic:
rw [Tendsto, ← coe_map]

Result:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ ↑(Ultrafilter.map (⇑(ConcreteCategory.hom f)) g) ≤ 𝓝 ((ConcreteCategory.hom f) x)

Proof state:
case a
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) g) = (ConcreteCategory.hom f) x

Tactic:
rw [← str_hom_commute, str_eq_of_le_nhds _ x _]

Result:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ ↑g ≤ 𝓝 x

Proof state:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ ↑(Ultrafilter.map (⇑(ConcreteCategory.hom f)) g) ≤ 𝓝 ((ConcreteCategory.hom f) x)

Tactic:
apply le_nhds_of_str_eq

Result:
case a
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) g) = (ConcreteCategory.hom f) x

Proof state:
X Y : Compactum
f : X ⟶ Y
⊢ ∀ (x : X.A) (g : Ultrafilter X.A),
    ↑g ≤ 𝓝 x → Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))

Tactic:
intro x g h

Result:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
h : ↑g ≤ 𝓝 x
⊢ Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))

Proof state:
X Y : Compactum
f : X ⟶ Y
⊢ Continuous ⇑(ConcreteCategory.hom f)

Tactic:
rw [continuous_iff_ultrafilter]

Result:
X Y : Compactum
f : X ⟶ Y
⊢ ∀ (x : X.A) (g : Ultrafilter X.A),
    ↑g ≤ 𝓝 x → Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))
-- Mathlib/RingTheory/Ideal/Basic.lean
theorem add_pow_add_pred_mem_of_pow_mem_of_commute  {m n : ℕ}
    (ha : a ^ m ∈ I) (hb : b ^ n ∈ I) (hab : Commute a b) :
    (a + b) ^ (m + n - 1) ∈ I :=
  I.add_pow_mem_of_pow_mem_of_le_of_commute ha hb (by rw [← Nat.sub_le_iff_le_add]) hab

Proof state:
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hab : Commute a b
⊢ m + n ≤ m + n - 1 + 1

Tactic:
rw [← Nat.sub_le_iff_le_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_add_negSucc (m n k : Nat) :
    subNatNat m n + -[k+1] = subNatNat m (n + succ k)

Proof state:
case inl
m n k : Nat
h' : m < n
h₂ : m < n + k.succ
⊢ -[(n - m).pred+1] + -[k+1] = -[(n + k.succ - m).pred+1]

Tactic:
simp only [pred_eq_sub_one, negSucc_add_negSucc, succ_eq_add_one, negSucc.injEq]

Result:
case inl
m n k : Nat
h' : m < n
h₂ : m < n + k.succ
⊢ n - m - 1 + k + 1 = n + (k + 1) - m - 1

Proof state:
m n k : Nat
h : m < n ∨ m ≥ n
⊢ subNatNat m n + -[k+1] = subNatNat m (n + k.succ)

Tactic:
cases h with
| inr h' =>
  rw [subNatNat_of_le h']
  simp
  rw [subNatNat_sub h', Nat.add_comm]
| inl h' =>
  have h₂ : m < n + succ k := Nat.lt_of_lt_of_le h' (le_add_right _ _)
  rw [subNatNat_of_lt h', subNatNat_of_lt h₂]
  simp only [pred_eq_sub_one, negSucc_add_negSucc, succ_eq_add_one, negSucc.injEq]
  rw [Nat.add_right_comm, sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h'), Nat.sub_sub,
    ← Nat.add_assoc, succ_sub_succ_eq_sub, Nat.add_comm n,Nat.add_sub_assoc (Nat.le_of_lt h'),
    Nat.add_comm]

Result:
no goals

Proof state:
case inl
m n k : Nat
h' : m < n
h₂ : m < n + k.succ
⊢ subNatNat m n + -[k+1] = subNatNat m (n + k.succ)

Tactic:
rw [subNatNat_of_lt h', subNatNat_of_lt h₂]

Result:
case inl
m n k : Nat
h' : m < n
h₂ : m < n + k.succ
⊢ -[(n - m).pred+1] + -[k+1] = -[(n + k.succ - m).pred+1]

Proof state:
case inr
m n k : Nat
h' : m ≥ n
⊢ ↑(m - n) + -[k+1] = subNatNat m (n + k.succ)

Tactic:
simp

Result:
case inr
m n k : Nat
h' : m ≥ n
⊢ subNatNat (m - n) (k + 1) = subNatNat m (n + (k + 1))

Proof state:
case inl
m n k : Nat
h' : m < n
h₂ : m < n + k.succ
⊢ n - m - 1 + k + 1 = n + (k + 1) - m - 1

Tactic:
rw [Nat.add_right_comm, sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h'), Nat.sub_sub,
  ← Nat.add_assoc, succ_sub_succ_eq_sub, Nat.add_comm n,Nat.add_sub_assoc (Nat.le_of_lt h'),
  Nat.add_comm]

Result:
no goals

Proof state:
m n k : Nat
⊢ subNatNat m n + -[k+1] = subNatNat m (n + k.succ)

Tactic:
have h := Nat.lt_or_ge m n

Result:
m n k : Nat
h : m < n ∨ m ≥ n
⊢ subNatNat m n + -[k+1] = subNatNat m (n + k.succ)

Proof state:
case inr
m n k : Nat
h' : m ≥ n
⊢ subNatNat m n + -[k+1] = subNatNat m (n + k.succ)

Tactic:
rw [subNatNat_of_le h']

Result:
case inr
m n k : Nat
h' : m ≥ n
⊢ ↑(m - n) + -[k+1] = subNatNat m (n + k.succ)

Proof state:
case inr
m n k : Nat
h' : m ≥ n
⊢ subNatNat (m - n) (k + 1) = subNatNat m (n + (k + 1))

Tactic:
rw [subNatNat_sub h', Nat.add_comm]

Result:
no goals

Proof state:
case inl
m n k : Nat
h' : m < n
⊢ subNatNat m n + -[k+1] = subNatNat m (n + k.succ)

Tactic:
have h₂ : m < n + succ k := Nat.lt_of_lt_of_le h' (le_add_right _ _)

Result:
case inl
m n k : Nat
h' : m < n
h₂ : m < n + k.succ
⊢ subNatNat m n + -[k+1] = subNatNat m (n + k.succ)
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem coeff_inv_units (u : R[X]ˣ) (n : ℕ) : ((↑u : R[X]).coeff n)⁻¹ = (↑u⁻¹ : R[X]).coeff n

Proof state:
case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ eval 0 ↑1 = 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
⊢ ((↑u).coeff n)⁻¹ = (↑u⁻¹).coeff n

Tactic:
rw [eq_C_of_degree_eq_zero (degree_coe_units u), eq_C_of_degree_eq_zero (degree_coe_units u⁻¹),
  coeff_C, coeff_C, inv_eq_one_div]

Result:
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
⊢ (1 / if n = 0 then (↑u).coeff 0 else 0) = if n = 0 then (↑u⁻¹).coeff 0 else 0

Proof state:
case neg
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : ¬n = 0
⊢ 1 / 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ 1 / (↑u).coeff 0 = (↑u⁻¹).coeff 0

Tactic:
rw [div_eq_iff_mul_eq (coeff_coe_units_zero_ne_zero u), coeff_zero_eq_eval_zero,
    coeff_zero_eq_eval_zero, ← eval_mul, ← Units.val_mul, inv_mul_cancel]

Result:
case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ eval 0 ↑1 = 1

Proof state:
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
⊢ (1 / if n = 0 then (↑u).coeff 0 else 0) = if n = 0 then (↑u⁻¹).coeff 0 else 0

Tactic:
split_ifs

Result:
case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ 1 / (↑u).coeff 0 = (↑u⁻¹).coeff 0

case neg
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : ¬n = 0
⊢ 1 / 0 = 0