harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem power_sum {ι} (a : Cardinal) (f : ι → Cardinal) :
    a ^ sum f = prod fun i ↦ a ^ f i

Proof state:
case h.h.e
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
⊢ ((i : ι) × Quotient.out #(f i) → α) ≃ ((i : ι) → Quotient.out #(f i → α))

Tactic:
refine (Equiv.piCurry fun _ _ => α).trans ?_

Result:
case h.h.e
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
⊢ ((a : ι) → Quotient.out #(f a) → α) ≃ ((i : ι) → Quotient.out #(f i → α))

Proof state:
case h.h
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
⊢ (#α ^ sum fun i => #(f i)) = prod fun i => #α ^ (fun i => #(f i)) i

Tactic:
simp_rw [prod, sum, power_def]

Result:
case h.h
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
⊢ #((i : ι) × Quotient.out #(f i) → α) = #((i : ι) → Quotient.out #(f i → α))

Proof state:
case h
ι : Type u_1
f : ι → Cardinal.{max u_1 u_2}
α : Type (max u_1 u_2)
⊢ #α ^ sum f = prod fun i => #α ^ f i

Tactic:
induction f using induction_on_pi with | _ f =>
simp_rw [prod, sum, power_def]
apply mk_congr
refine (Equiv.piCurry fun _ _ => α).trans ?_
refine Equiv.piCongrRight fun b => ?_
refine (Equiv.arrowCongr outMkEquiv (Equiv.refl α)).trans ?_
exact outMkEquiv.symm

Result:
no goals

Proof state:
case h.h.e
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
b : ι
⊢ (f b → α) ≃ Quotient.out #(f b → α)

Tactic:
exact outMkEquiv.symm

Result:
no goals

Proof state:
case h.h.e
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
⊢ ((a : ι) → Quotient.out #(f a) → α) ≃ ((i : ι) → Quotient.out #(f i → α))

Tactic:
refine Equiv.piCongrRight fun b => ?_

Result:
case h.h.e
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
b : ι
⊢ (Quotient.out #(f b) → α) ≃ Quotient.out #(f b → α)

Proof state:
ι : Type u_1
a : Cardinal.{max u_1 u_2}
f : ι → Cardinal.{max u_1 u_2}
⊢ a ^ sum f = prod fun i => a ^ f i

Tactic:
induction a using Cardinal.inductionOn with | _ α =>
induction f using induction_on_pi with | _ f =>
simp_rw [prod, sum, power_def]
apply mk_congr
refine (Equiv.piCurry fun _ _ => α).trans ?_
refine Equiv.piCongrRight fun b => ?_
refine (Equiv.arrowCongr outMkEquiv (Equiv.refl α)).trans ?_
exact outMkEquiv.symm

Result:
no goals

Proof state:
case h.h
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
⊢ #((i : ι) × Quotient.out #(f i) → α) = #((i : ι) → Quotient.out #(f i → α))

Tactic:
apply mk_congr

Result:
case h.h.e
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
⊢ ((i : ι) × Quotient.out #(f i) → α) ≃ ((i : ι) → Quotient.out #(f i → α))

Proof state:
case h.h.e
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
b : ι
⊢ (Quotient.out #(f b) → α) ≃ Quotient.out #(f b → α)

Tactic:
refine (Equiv.arrowCongr outMkEquiv (Equiv.refl α)).trans ?_

Result:
case h.h.e
ι : Type u_1
α : Type (max u_1 u_2)
f : ι → Type (max u_1 u_2)
b : ι
⊢ (f b → α) ≃ Quotient.out #(f b → α)
-- Mathlib/Order/CompleteLattice/SetLike.lean
@[simp] lemma mem_sInf : x ∈ sInf 𝒮 ↔ ∀ T ∈ 𝒮, x ∈ T

Proof state:
X : Type u_1
L : CompleteSublattice (Set X)
𝒮 : Set ↥L
x : X
⊢ x ∈ sInf 𝒮 ↔ ∀ T ∈ 𝒮, x ∈ T

Tactic:
simp [← mem_subtype]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Positive.lean
theorem IsPositive.conj_adjoint {T : E →L[𝕜] E} (hT : T.IsPositive) (S : E →L[𝕜] F) :
    (S ∘L T ∘L S†).IsPositive

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
x : F
⊢ 0 ≤ (S.comp (T.comp (adjoint S))).reApplyInnerSelf x

Tactic:
rw [reApplyInnerSelf, comp_apply, ← adjoint_inner_right]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
x : F
⊢ 0 ≤ re ⟪(T.comp (adjoint S)) x, (adjoint S) x⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
x : F
⊢ 0 ≤ re ⟪(T.comp (adjoint S)) x, (adjoint S) x⟫_𝕜

Tactic:
exact hT.inner_nonneg_left _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
⊢ (S.comp (T.comp (adjoint S))).IsPositive

Tactic:
refine ⟨hT.isSelfAdjoint.conj_adjoint S, fun x => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
x : F
⊢ 0 ≤ (S.comp (T.comp (adjoint S))).reApplyInnerSelf x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem mk_add_mem_zipIdx_iff_getElem? {k i : Nat} {x : α} {l : Array α} :
    (x, k + i) ∈ zipIdx l k ↔ l[i]? = some x

Proof state:
α : Type u_1
k i : Nat
x : α
l : Array α
⊢ (x, k + i) ∈ l.zipIdx k ↔ l[i]? = some x

Tactic:
simp [mem_iff_getElem?, and_left_comm]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Extend.lean
theorem norm_extendTo𝕜'_apply_sq (fr : F →ₗ[ℝ] ℝ) (x : F) :
    ‖(fr.extendTo𝕜' x : 𝕜)‖ ^ 2 = fr (conj (fr.extendTo𝕜' x : 𝕜) • x) :=
  calc
    ‖(fr.extendTo𝕜' x : 𝕜)‖ ^ 2 = re (conj (fr.extendTo𝕜' x) * fr.extendTo𝕜' x : 𝕜)

Proof state:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ re ((starRingEnd 𝕜) (fr.extendTo𝕜' x) * fr.extendTo𝕜' x) = fr ((starRingEnd 𝕜) (fr.extendTo𝕜' x) • x)

Tactic:
rw [← smul_eq_mul, ← map_smul, extendTo𝕜'_apply_re]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ ‖fr.extendTo𝕜' x‖ ^ 2 = re ((starRingEnd 𝕜) (fr.extendTo𝕜' x) * fr.extendTo𝕜' x)

Tactic:
rw [RCLike.conj_mul, ← ofReal_pow, ofReal_re]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
protected lemma id {p : 𝒳 ⥤ 𝒮} {R : 𝒮} {a : 𝒳} (ha : p.obj a = R) : p.IsHomLift (𝟙 R) (𝟙 a)

Proof state:
case refl
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (𝟙 a)

Tactic:
infer_instance

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R : 𝒮
a : 𝒳
ha : p.obj a = R
⊢ p.IsHomLift (𝟙 R) (𝟙 a)

Tactic:
cases ha

Result:
case refl
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (𝟙 a)
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `mul_inv_lt_iff₀` for a version with multiplication on the other side. -/
lemma mul_inv_lt_iff₀' (hc : 0 < c) : b * c⁻¹ < a ↔ b < c * a

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ < a ↔ b < c * a

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
this : MulPosStrictMono G₀
⊢ b * c⁻¹ < a ↔ b < c * a

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
this : MulPosStrictMono G₀
⊢ b * c⁻¹ < a ↔ b < c * a

Tactic:
rw [mul_inv_lt_iff₀ hc, mul_comm]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_union_eq_adjoin_adjoin :
    adjoin R (s ∪ t) = (adjoin (adjoin R s) t).restrictScalars R

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ adjoin R (s ∪ t) = Subalgebra.restrictScalars R (adjoin (↥(adjoin R s)) t)

Tactic:
simpa using adjoin_algebraMap_image_union_eq_adjoin_adjoin R s t

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem neg_right {N : Type*} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N]
    {v : VectorMeasure α M} {w : VectorMeasure α N} (h : v ≪ᵥ w) : v ≪ᵥ -w

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑(-w) s = 0
⊢ ↑v s = 0

Tactic:
rw [neg_apply, neg_eq_zero] at hs

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑v s = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
⊢ v ≪ᵥ -w

Tactic:
intro s hs

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑(-w) s = 0
⊢ ↑v s = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
N : Type u_6
inst✝² : AddCommGroup N
inst✝¹ : TopologicalSpace N
inst✝ : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑v s = 0

Tactic:
exact h hs

Result:
no goals
-- Mathlib/Order/Interval/Basic.lean
theorem disjoint_coe (s t : Interval α) : Disjoint (s : Set α) t ↔ Disjoint s t

Proof state:
α : Type u_1
inst✝ : Lattice α
s t : Interval α
⊢ ↑s ⊓ ↑t ≤ ⊥ ↔ ↑s ∩ ↑t ⊆ ↑⊥

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Lattice α
s t : Interval α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
classical
  rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
  rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Lattice α
s t : Interval α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]

Result:
α : Type u_1
inst✝ : Lattice α
s t : Interval α
⊢ ↑s ⊓ ↑t ≤ ⊥ ↔ ↑s ∩ ↑t ⊆ ↑⊥
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem contDiffOn_nat_iff_continuousOn_differentiableOn_deriv {n : ℕ} (hs : UniqueDiffOn 𝕜 s) :
    ContDiffOn 𝕜 n f s ↔ (∀ m : ℕ, m ≤ n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ m : ℕ, m < n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (↑n) f s ↔
    (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s

Tactic:
rw [show n = ((n : ℕ∞) : WithTop ℕ∞) from rfl,
  contDiffOn_iff_continuousOn_differentiableOn_deriv hs]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ((∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ↔
    (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ((∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) ↔
    (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem lt_add_of_tsub_lt_left (hb : AddLECancellable b) (h : a - b < c) : a < b + c

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
⊢ a ≠ b + c

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hb : AddLECancellable b
h : b + c - b < c
⊢ False

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hb : AddLECancellable b
h : b + c - b < c
⊢ False

Tactic:
simp [hb] at h

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
⊢ a < b + c

Tactic:
rw [lt_iff_le_and_ne, ← tsub_le_iff_left]

Result:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
⊢ a - b ≤ c ∧ a ≠ b + c

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
⊢ a - b ≤ c ∧ a ≠ b + c

Tactic:
refine ⟨h.le, ?_⟩

Result:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
⊢ a ≠ b + c
-- Mathlib/Data/Finset/Max.lean
theorem max'_singleton (a : α) : ({a} : Finset α).max' (singleton_nonempty _) = a

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.max' ⋯ = a

Tactic:
simp [max']

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Supported.lean
theorem supported_empty : supported R (∅ : Set σ) = ⊥

Proof state:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
⊢ supported R ∅ = ⊥

Tactic:
simp [supported_eq_adjoin_X]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem normSq_pos {z : K} : 0 < normSq z ↔ z ≠ 0

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < normSq z ↔ z ≠ 0

Tactic:
rw [lt_iff_le_and_ne, Ne, eq_comm]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ normSq z ∧ ¬normSq z = 0 ↔ z ≠ 0

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ normSq z ∧ ¬normSq z = 0 ↔ z ≠ 0

Tactic:
simp [normSq_nonneg]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem min {p : A[X]} (pmonic : p.Monic) (hp : Polynomial.aeval x p = 0) :
    degree (minpoly A x) ≤ degree p

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
⊢ (minpoly A x).degree ≤ p.degree

Tactic:
delta minpoly

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
⊢ (if hx : IsIntegral A x then ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0).degree ≤
    p.degree

Proof state:
case pos
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
hx : IsIntegral A x
⊢ (⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).degree ≤ p.degree

Tactic:
exact le_of_not_lt (degree_lt_wf.not_lt_min _ hx ⟨pmonic, hp⟩)

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
⊢ (if hx : IsIntegral A x then ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0).degree ≤
    p.degree

Tactic:
split_ifs with hx

Result:
case pos
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
hx : IsIntegral A x
⊢ (⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).degree ≤ p.degree

case neg
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
hx : ¬IsIntegral A x
⊢ degree 0 ≤ p.degree

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
hx : ¬IsIntegral A x
⊢ degree 0 ≤ p.degree

Tactic:
simp only [degree_zero, bot_le]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem IsRelPrime.ne_zero_or_ne_zero [Nontrivial α] (h : IsRelPrime x y) : x ≠ 0 ∨ y ≠ 0 :=
  not_or_of_imp <| by rintro rfl rfl; exact not_isRelPrime_zero_zero h

Proof state:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
x y : α
inst✝ : Nontrivial α
h : IsRelPrime x y
⊢ x = 0 → y ≠ 0

Tactic:
rintro rfl rfl

Result:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
h : IsRelPrime 0 0
⊢ False

Proof state:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Nontrivial α
h : IsRelPrime 0 0
⊢ False

Tactic:
exact not_isRelPrime_zero_zero h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem map_dvd_map [Ring S] (f : R →+* S) (hf : Function.Injective f) {x y : R[X]}
    (hx : x.Monic) : x.map f ∣ y.map f ↔ x ∣ y

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
rw [← modByMonic_eq_zero_iff_dvd hx, ← modByMonic_eq_zero_iff_dvd (hx.map f), ←
  map_modByMonic f hx]

Result:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f (y %ₘ x) = 0 ↔ y %ₘ x = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
H : y %ₘ x = 0
⊢ map f (y %ₘ x) = 0

Tactic:
rw [H, Polynomial.map_zero]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
H : map f (y %ₘ x) = 0
⊢ map f (y %ₘ x) = map f 0

Tactic:
rw [H, Polynomial.map_zero]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f (y %ₘ x) = 0 ↔ y %ₘ x = 0

Tactic:
exact
  ⟨fun H => map_injective f hf <| by rw [H, Polynomial.map_zero], fun H => by
    rw [H, Polynomial.map_zero]⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkGateCached_le_size (aig : AIG α) (input : GateInput aig)
    : aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
⊢ aig.decls.size ≤
    (if input.lhs.ref.gate < input.rhs.ref.gate then mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }
          else mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls.size

Tactic:
split

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
h✝ : input.lhs.ref.gate < input.rhs.ref.gate
⊢ aig.decls.size ≤ (mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }).aig.decls.size

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
⊢ aig.decls.size ≤ (mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls.size

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
h✝ : ¬input.lhs.ref.gate < input.rhs.ref.gate
⊢ aig.decls.size ≤ (mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls.size

Tactic:
apply mkGateCached.go_le_size

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
⊢ aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size

Tactic:
dsimp only [mkGateCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
⊢ aig.decls.size ≤
    (if input.lhs.ref.gate < input.rhs.ref.gate then mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }
          else mkGateCached.go aig { lhs := input.rhs, rhs := input.lhs }).aig.decls.size

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
h✝ : input.lhs.ref.gate < input.rhs.ref.gate
⊢ aig.decls.size ≤ (mkGateCached.go aig { lhs := input.lhs, rhs := input.rhs }).aig.decls.size

Tactic:
apply mkGateCached.go_le_size

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_singleton_inter [DecidableEq α] : #({a} ∩ s) ≤ 1

Proof state:
case isFalse
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #({a} ∩ s) ≤ 1

Tactic:
simp [Finset.singleton_inter_of_not_mem h]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #({a} ∩ s) ≤ 1

Tactic:
simp [Finset.singleton_inter_of_mem h]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #({a} ∩ s) ≤ 1

Tactic:
obtain h | h := Finset.decidableMem a s

Result:
case isFalse
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #({a} ∩ s) ≤ 1

case isTrue
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #({a} ∩ s) ≤ 1
-- Mathlib/Analysis/RCLike/Basic.lean
theorem I_mul_re (z : K) : re (I * z) = -im z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re (I * z) = -im z

Tactic:
simp only [I_re, zero_sub, I_im', zero_mul, mul_re]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_mul_lt_one_iff_lt : a * b⁻¹ < 1 ↔ a < b

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ a * b⁻¹ < 1 ↔ a < b

Tactic:
rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right, one_mul]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma one_le_dual_one :
    1 ≤ dual A K (1 : FractionalIdeal B⁰ L) :=
  le_dual_inv_aux A K one_ne_zero (by rw [one_mul])

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ 1 * 1 ≤ 1

Tactic:
rw [one_mul]

Result:
no goals