harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.induction {t} (hl : @Sized α t) {C : Ordnode α → Prop} (H0 : C nil)
    (H1 : ∀ l x r, C l → C r → C (.node' l x r)) : C t

Proof state:
case node
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l : l✝.Sized → C l✝
t_ih_r : r✝.Sized → C r✝
hl : (node size✝ l✝ x✝ r✝).Sized
⊢ C (l✝.node' x✝ r✝)

Tactic:
exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)

Result:
no goals

Proof state:
case nil
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
hl : nil.Sized
⊢ C nil

Tactic:
exact H0

Result:
no goals

Proof state:
case node
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l : l✝.Sized → C l✝
t_ih_r : r✝.Sized → C r✝
hl : (node size✝ l✝ x✝ r✝).Sized
⊢ C (node size✝ l✝ x✝ r✝)

Tactic:
rw [hl.eq_node']

Result:
case node
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l : l✝.Sized → C l✝
t_ih_r : r✝.Sized → C r✝
hl : (node size✝ l✝ x✝ r✝).Sized
⊢ C (l✝.node' x✝ r✝)

Proof state:
α : Type u_1
t : Ordnode α
hl : t.Sized
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
⊢ C t

Tactic:
induction t with
| nil => exact H0
| node _ _ _ _ t_ih_l t_ih_r =>
  rw [hl.eq_node']
  exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
@[simp]
lemma iSup_iff {ι : Sort*} (W : ι → MorphismProperty C) {X Y : C} (f : X ⟶ Y) :
    iSup W f ↔ ∃ i, W i f

Proof state:
case mpr.intro
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
i : ι
hf : W i f
⊢ ∃ W_1, ↑W_1 f

Tactic:
exact ⟨⟨_, i, rfl⟩, hf⟩

Result:
no goals

Proof state:
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
i : ι
hf : ↑⟨W i, ⋯⟩ f
⊢ ∃ i, W i f

Tactic:
exact ⟨i, hf⟩

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∃ W_1, ↑W_1 f) → ∃ i, W i f

Tactic:
rintro ⟨⟨_, i, rfl⟩, hf⟩

Result:
case mp.intro.mk.intro
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
i : ι
hf : ↑⟨W i, ⋯⟩ f
⊢ ∃ i, W i f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∃ W_1, ↑W_1 f) ↔ ∃ i, W i f

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∃ W_1, ↑W_1 f) → ∃ i, W i f

case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∃ i, W i f) → ∃ W_1, ↑W_1 f

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∃ i, W i f) → ∃ W_1, ↑W_1 f

Tactic:
rintro ⟨i, hf⟩

Result:
case mpr.intro
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
i : ι
hf : W i f
⊢ ∃ W_1, ↑W_1 f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ iSup W f ↔ ∃ i, W i f

Tactic:
apply (sSup_iff (Set.range W) f).trans

Result:
C : Type u
inst✝ : Category.{v, u} C
ι : Sort u_2
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∃ W_1, ↑W_1 f) ↔ ∃ i, W i f
-- Mathlib/RingTheory/Ideal/Quotient/Index.lean
/-- Let `N` be a finite index f.g. `R`-submodule, and `I` be a finite index ideal.
Then `I • N` also has finite index. -/
lemma Submodule.finite_quotient_smul [Finite (R ⧸ I)] [Finite (M ⧸ N)] (hN : N.FG) :
    Finite (M ⧸ I • N)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≠ 0

Tactic:
have : Module.Finite R N := Module.Finite.iff_fg.mpr hN

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
N : Submodule R M
inst✝¹ : Finite (R ⧸ I)
inst✝ : Finite (M ⧸ N)
hN : N.FG
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
this : Module.Finite R ↥N
⊢ Nat.card ((R ⧸ I) ⊗[R] ↥N) ≠ 0
-- Mathlib/Data/Seq/Computation.lean
theorem LiftRel.equiv (R : α → α → Prop) : Equivalence R → Equivalence (LiftRel R)
  | ⟨refl, symm, trans⟩ => ⟨LiftRel.refl R refl, by apply LiftRel.symm; apply symm,
    by apply LiftRel.trans; apply trans⟩

Proof state:
α : Type u
R : α → α → Prop
refl : ∀ (x : α), R x x
symm : ∀ {x y : α}, R x y → R y x
trans : ∀ {x y z : α}, R x y → R y z → R x z
⊢ ∀ {x y z : Computation α}, LiftRel R x y → LiftRel R y z → LiftRel R x z

Tactic:
apply LiftRel.trans

Result:
case H
α : Type u
R : α → α → Prop
refl : ∀ (x : α), R x x
symm : ∀ {x y : α}, R x y → R y x
trans : ∀ {x y z : α}, R x y → R y z → R x z
⊢ Transitive R

Proof state:
case H
α : Type u
R : α → α → Prop
refl : ∀ (x : α), R x x
symm : ∀ {x y : α}, R x y → R y x
trans : ∀ {x y z : α}, R x y → R y z → R x z
⊢ Transitive R

Tactic:
apply trans

Result:
no goals

Proof state:
case H
α : Type u
R : α → α → Prop
refl : ∀ (x : α), R x x
symm : ∀ {x y : α}, R x y → R y x
trans : ∀ {x y z : α}, R x y → R y z → R x z
⊢ Symmetric R

Tactic:
apply symm

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
refl : ∀ (x : α), R x x
symm : ∀ {x y : α}, R x y → R y x
trans : ∀ {x y z : α}, R x y → R y z → R x z
⊢ ∀ {x y : Computation α}, LiftRel R x y → LiftRel R y x

Tactic:
apply LiftRel.symm

Result:
case H
α : Type u
R : α → α → Prop
refl : ∀ (x : α), R x x
symm : ∀ {x y : α}, R x y → R y x
trans : ∀ {x y z : α}, R x y → R y z → R x z
⊢ Symmetric R
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ico_add_one_left_eq_Ioo (a b : α) : Ico (a + 1) b = Ioo a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
⊢ Ico (a + 1) b = Ioo a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_left_eq_Ioo a b

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem exists_primitive_element_lt_of_isComplex {w₀ : InfinitePlace K} (hw₀ : IsComplex w₀)
    {B : ℝ≥0} (hB : minkowskiBound K ↑1 < convexBodyLT'Factor K * B) :
    ∃ a : 𝓞 K, ℚ⟮(a : K)⟯ = ⊤ ∧
      ∀ w : InfinitePlace K, w a < Real.sqrt (1 + B ^ 2)

Proof state:
case intro.intro.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w => if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ :
  |((↑⟨w₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
⊢ w ↑a < √(1 + ↑B ^ 2)

Tactic:
by_cases h_eq : w = w₀

Result:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w => if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ :
  |((↑⟨w₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w => if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ :
  |((↑⟨w₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : ¬w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)

Proof state:
case pos.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w => if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ |(w₀.embedding ↑a).re| < 1

Tactic:
exact h_le₀.1

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/PolynomialExp.lean
theorem tendsto_div_exp_atTop (p : ℝ[X]) : Tendsto (fun x ↦ p.eval x / exp x) atTop (𝓝 0)

Proof state:
case h_add
p q : ℝ[X]
hp : Tendsto (fun x => eval x p / rexp x) atTop (𝓝 0)
hq : Tendsto (fun x => eval x q / rexp x) atTop (𝓝 0)
⊢ Tendsto (fun x => eval x (p + q) / rexp x) atTop (𝓝 0)

Tactic:
simpa [add_div] using hp.add hq

Result:
no goals

Proof state:
p : ℝ[X]
⊢ Tendsto (fun x => eval x p / rexp x) atTop (𝓝 0)

Tactic:
induction p using Polynomial.induction_on' with
| h_monomial n c => simpa [exp_neg, div_eq_mul_inv, mul_assoc]
  using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_zero n)
| h_add p q hp hq => simpa [add_div] using hp.add hq

Result:
no goals

Proof state:
case h_monomial
n : ℕ
c : ℝ
⊢ Tendsto (fun x => eval x ((monomial n) c) / rexp x) atTop (𝓝 0)

Tactic:
simpa [exp_neg, div_eq_mul_inv, mul_assoc]
using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_zero n)

Result:
no goals
-- Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean
/-- Tailored version for even Jacobi theta functions. -/
lemma hasSum_mellin_pi_mul_sq {a : ι → ℂ} {r : ι → ℝ} {F : ℝ → ℂ} {s : ℂ} (hs : 0 < s.re)
    (hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * rexp (-π * r i ^ 2 * t)) (F t))
    (h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re) :
    HasSum (fun i ↦ Gammaℝ s * a i / |r i| ^ s) (mellin F (s / 2))

Proof state:
case h.e'_5.h.h.e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑(r i ^ 2) ^ (s / 2)

Tactic:
rw [← sq_abs, ofReal_pow, ← cpow_nat_mul']

Result:
case h.e'_5.h.h.e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑|r i| ^ (↑2 * (s / 2))

case h.e'_5.h.h.e'_6.hlt
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ -π < ↑2 * (↑|r i|).arg

case h.e'_5.h.h.e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * (↑|r i|).arg ≤ π

Proof state:
case h.e'_5.h.h.e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑|r i| ^ (↑2 * (s / 2))

Tactic:
ring_nf

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem univ_pi_ite (s : Set ι) [DecidablePred (· ∈ s)] (t : ∀ i, Set (α i)) :
    (pi univ fun i => if i ∈ s then t i else univ) = s.pi t

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ (∀ (i : ι), x✝ i ∈ if i ∈ s then t i else univ) ↔ x✝ ∈ s.pi t

Tactic:
refine forall_congr' fun i => ?_

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
i : ι
⊢ (x✝ i ∈ if i ∈ s then t i else univ) ↔ i ∈ s → x✝ i ∈ t i

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
i : ι
⊢ (x✝ i ∈ if i ∈ s then t i else univ) ↔ i ∈ s → x✝ i ∈ t i

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
⊢ (univ.pi fun i => if i ∈ s then t i else univ) = s.pi t

Tactic:
ext

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ (x✝ ∈ univ.pi fun i => if i ∈ s then t i else univ) ↔ x✝ ∈ s.pi t

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ (x✝ ∈ univ.pi fun i => if i ∈ s then t i else univ) ↔ x✝ ∈ s.pi t

Tactic:
simp_rw [mem_univ_pi]

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ (∀ (i : ι), x✝ i ∈ if i ∈ s then t i else univ) ↔ x✝ ∈ s.pi t
-- Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
lemma CFC.monotoneOn_one_sub_one_add_inv :
    MonotoneOn (cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹)) (Set.Ici (0 : A))

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : autoParam (0 ≤ c) _auto✝
x : ℝ≥0
x✝ : x ∈ σ ℝ≥0 c
⊢ id (1 + x) ≠ 0

Tactic:
dsimp only [id]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : autoParam (0 ≤ c) _auto✝
x : ℝ≥0
x✝ : x ∈ σ ℝ≥0 c
⊢ 1 + x ≠ 0

Proof state:
case funProp.discharger
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : autoParam (0 ≤ c) _auto✝
x✝ : ℝ≥0
a✝ : x✝ ∈ σ ℝ≥0 c
⊢ 1 + x✝ ≠ 0

Tactic:
positivity

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.inv_mul_cancel_right` for a simpler version assuming `b ≠ 0`, `b ≠ ∞`. -/
protected lemma inv_mul_cancel_right' (hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) :
    a * b⁻¹ * b = a

Proof state:
case inr.inl
a : ℝ≥0∞
hb₀✝ : ⊤ = 0 → a = 0
hb : ⊤ = ⊤ → a = 0
hb₀ : ⊤ ≠ 0
⊢ a * ⊤⁻¹ * ⊤ = a

Tactic:
simp_all

Result:
no goals

Proof state:
case inl
a : ℝ≥0∞
hb₀ : 0 = 0 → a = 0
hb : 0 = ⊤ → a = 0
⊢ a * 0⁻¹ * 0 = a

Tactic:
simp_all

Result:
no goals

Proof state:
a b : ℝ≥0∞
hb₀ : b = 0 → a = 0
hb : b = ⊤ → a = 0
⊢ a * b⁻¹ * b = a

Tactic:
obtain rfl | hb₀ := eq_or_ne b 0

Result:
case inl
a : ℝ≥0∞
hb₀ : 0 = 0 → a = 0
hb : 0 = ⊤ → a = 0
⊢ a * 0⁻¹ * 0 = a

case inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb : b = ⊤ → a = 0
hb₀ : b ≠ 0
⊢ a * b⁻¹ * b = a

Proof state:
case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ⊤ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ a * b⁻¹ * b = a

Tactic:
simp [mul_assoc, ENNReal.inv_mul_cancel, *]

Result:
no goals

Proof state:
case inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb : b = ⊤ → a = 0
hb₀ : b ≠ 0
⊢ a * b⁻¹ * b = a

Tactic:
obtain rfl | hb := eq_or_ne b ⊤

Result:
case inr.inl
a : ℝ≥0∞
hb₀✝ : ⊤ = 0 → a = 0
hb : ⊤ = ⊤ → a = 0
hb₀ : ⊤ ≠ 0
⊢ a * ⊤⁻¹ * ⊤ = a

case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ⊤ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ a * b⁻¹ * b = a
-- Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
lemma universallyClosed_eq_universallySpecializing :
    @UniversallyClosed = (topologically @SpecializingMap).universally ⊓ @QuasiCompact

Proof state:
case a

⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ (topologically @IsClosedMap).universally

Tactic:
exact universally_mono fun X Y f ⟨h₁, h₂⟩ ↦ (isClosedMap_iff_specializingMap _).mpr h₁

Result:
no goals

Proof state:
case a

⊢ @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
rw [← universally_eq_iff (P := @UniversallyClosed).mpr inferInstance]

Result:
case a

⊢ universally @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Proof state:
case a

⊢ universally @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
exact universally_mono fun X Y f H ↦ ⟨f.isClosedMap.specializingMap, inferInstance⟩

Result:
no goals

Proof state:
⊢ @UniversallyClosed = (topologically @SpecializingMap).universally ⊓ @QuasiCompact

Tactic:
rw [← universally_eq_iff (P := @QuasiCompact).mpr inferInstance, ← universally_inf]

Result:
⊢ @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Proof state:
case a

⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ @UniversallyClosed

Tactic:
rw [universallyClosed_eq]

Result:
case a

⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ (topologically @IsClosedMap).universally

Proof state:
⊢ @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
apply le_antisymm

Result:
case a

⊢ @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally

case a

⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ @UniversallyClosed
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem germ_toOpen
    (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R) (hx : x ∈ U) (f : R) :
    (structureSheaf R).presheaf.germ U x hx (toOpen R U f) = toStalk R x f

Proof state:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
f : R
⊢ (ConcreteCategory.hom ((structureSheaf R).presheaf.germ U x hx)) ((ConcreteCategory.hom (toOpen R U)) f) =
    (ConcreteCategory.hom (toStalk R x)) f

Tactic:
rw [← toOpen_germ]

Result:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
f : R
⊢ (ConcreteCategory.hom ((structureSheaf R).presheaf.germ U x hx)) ((ConcreteCategory.hom (toOpen R U)) f) =
    (ConcreteCategory.hom (toOpen R ?U ≫ (structureSheaf R).presheaf.germ ?U x ?hx)) f

case U
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
f : R
⊢ Opens ↑(PrimeSpectrum.Top R)

case hx
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
f : R
⊢ x ∈ ?U

Proof state:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
f : R
⊢ (ConcreteCategory.hom ((structureSheaf R).presheaf.germ U x hx)) ((ConcreteCategory.hom (toOpen R U)) f) =
    (ConcreteCategory.hom (toOpen R ?U ≫ (structureSheaf R).presheaf.germ ?U x ?hx)) f

case U
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
f : R
⊢ Opens ↑(PrimeSpectrum.Top R)

case hx
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
f : R
⊢ x ∈ ?U

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_comp_iff {X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y) :
    eqToHom p ≫ g = f ↔ g = eqToHom p.symm ≫ f :=
  { mp := fun h => h ▸ by simp
    mpr := fun h => h ▸ by simp [whisker_eq _ h] }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : eqToHom p ≫ g = f
⊢ g = eqToHom ⋯ ≫ eqToHom p ≫ g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : g = eqToHom ⋯ ≫ f
⊢ eqToHom p ≫ eqToHom ⋯ ≫ f = f

Tactic:
simp [whisker_eq _ h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) (id : Nat) :
    StrongAssignmentsInvariant f → StrongAssignmentsInvariant (deleteOne f id)

Proof state:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl : ¬∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList

Tactic:
simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl

Result:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
-- Mathlib/Data/Nat/Cast/Basic.lean
@[simp] lemma _root_.nsmul_eq_mul (n : ℕ) (a : α) : n • a = n * a

Proof state:
case zero
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
⊢ 0 • a = ↑0 * a

Tactic:
rw [zero_nsmul, Nat.cast_zero, zero_mul]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NonAssocSemiring α
n : ℕ
a : α
⊢ n • a = ↑n * a

Tactic:
induction n with
| zero => rw [zero_nsmul, Nat.cast_zero, zero_mul]
| succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = ↑n * a
⊢ (n + 1) • a = ↑(n + 1) * a

Tactic:
rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]

Result:
no goals